Proof 01. 1 ⊢ x ∈ A ∪ B, hypo. 02. 1 ⊢ x ∈ A ∨ x ∈ B, union_elim 1. 03. 3 ⊢ x ∈ A, hypo. 04. 3 ⊢ x ∈ B ∪ A, union_intror 3. 05. 5 ⊢ x ∈ B, hypo. 06. 5 ⊢ x ∈ B ∪ A, union_introl 5. 07. 1 ⊢ x ∈ B ∪ A, disj_elim 2 4 6. 08. ⊢ x ∈ A ∪ B → x ∈ B ∪ A, subj_intro 7. 09. ⊢ x ∈ B ∪ A → x ∈ A ∪ B, 8. 10. ⊢ x ∈ A ∪ B ↔ x ∈ B ∪ A, bij_intro 8 9. 11. ⊢ ∀x. x ∈ A ∪ B ↔ x ∈ B ∪ A, uq_intro 10. union_comm. ⊢ A ∪ B = B ∪ A, ext 11.
Dependencies
The given proof depends on four axioms:
comp, eq_refl, eq_subst, ext.