Proof 01. 1 ⊢ x ∈ A ∩ B, hypo. 02. 1 ⊢ x ∈ A, intersection_eliml 1. 03. 1 ⊢ x ∈ B, intersection_elimr 1. 04. 1 ⊢ x ∈ B ∩ A, intersection_intro 3 2. 05. ⊢ x ∈ A ∩ B → x ∈ B ∩ A, subj_intro 4. 06. ⊢ x ∈ B ∩ A → x ∈ A ∩ B, 5. 07. ⊢ x ∈ A ∩ B ↔ x ∈ B ∩ A, bij_intro 5 6. 08. ⊢ ∀x. x ∈ A ∩ B ↔ x ∈ B ∩ A, uq_intro 7. intersection_comm. ⊢ A ∩ B = B ∩ A, ext 8.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.