The operation ⋂{x | P x} may be seen as an encoding of ιx. P x, read
"the unique x such that x has property P", which represents a
definite description. It originates from Russell's
Principia Mathematica, see vol. I, *14, page 181.
Proof sketch
By assumption, there exists exactly one x with P x, call it a.
Thus, the comprehension reduces to the singleton
{x | P x} = {a}.
So we have
u = ⋂{x | P x} = ⋂{a} = a.
But u = a means u ∈ {a}, thus u ∈ {x | P x}, and therefore
P u. q.e.d.
Proof
01. 1 ⊢ u = ⋂{x |P x}, hypo.
02. 2 ⊢ ∃a. set a ∧ ∀x. a = x ↔ P x, hypo.
03. 2 ⊢ ∃a. set a ∧ {a} = {x | P x}, sg_eq_from_ex_uniq 2.
04. 4 ⊢ set a ∧ {a} = {x | P x}, hypo.
05. 4 ⊢ set a, conj_eliml 4.
06. 4 ⊢ {a} = {x | P x}, conj_elimr 4.
07. 4 ⊢ ⋂{a} = ⋂{x | P x}, eq_cong 6, f t = ⋂t.
08. 1, 4 ⊢ u = ⋂{a}, eq_trans_rr 1 7.
09. 4 ⊢ ⋂{a} = a, Intersection_sg 5.
10. 1, 4 ⊢ u = a, eq_trans 8 9.
11. 1, 4 ⊢ u ∈ {a}, sg_intro 5 10.
12. 1, 4 ⊢ u ∈ {x | P x}, eq_subst 6 11, P t ↔ u ∈ t.
13. 1, 4 ⊢ P u, comp_elim 12.
14. 1, 2 ⊢ P u, ex_elim 3 13.
iota_elim. ⊢ u = ⋂{x |P x} → (∃a. set a ∧ ∀x. a = x ↔ P x) → P u,
subj_intro_ii 14.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.