union_neutl

Theorem union_neutl

Theorem. union_neutl
∅ ∪ A = A

Proof
01. 1 ⊢ x ∈ ∅ ∪ A, hypo.
02. 1 ⊢ x ∈ ∅ ∨ x ∈ A, union_elim 1.
03. 3 ⊢ x ∈ ∅, hypo.
04. 3 ⊢ x ∈ A, empty_efq 3.
05. 5 ⊢ x ∈ A, hypo.
06. 1 ⊢ x ∈ A, disj_elim 2 4 5.
07. ⊢ x ∈ ∅ ∪ A → x ∈ A, subj_intro 6.
08. 8 ⊢ x ∈ A, hypo.
09. 8 ⊢ x ∈ ∅ ∪ A, union_intror 8.
10. ⊢ x ∈ A → x ∈ ∅ ∪ A, subj_intro 9.
11. ⊢ x ∈ ∅ ∪ A ↔ x ∈ A, bij_intro 7 10.
12. ⊢ ∀x. x ∈ ∅ ∪ A ↔ x ∈ A, uq_intro 11.
union_neutl. ⊢ ∅ ∪ A = A, ext 12.

Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.