Proof
01. 1 ⊢ x ∈ A, hypo.
02. 2 ⊢ x ∈ B, hypo.
03. 1, 2 ⊢ x ∈ A ∧ x ∈ B, conj_intro 1 2.
04. 1 ⊢ set x, set_intro 1.
05. 1, 2 ⊢ x ∈ {x | x ∈ A ∧ x ∈ B}, comp_intro 4 3.
06. 1, 2 ⊢ x ∈ A ∩ B, eq_subst_rev intersection_eq 5, P u ↔ x ∈ u.
intersection_intro. ⊢ x ∈ A → x ∈ B → x ∈ A ∩ B, subj_intro_ii 6.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.