Proof
01. 1 ⊢ x ∈ A ∨ x ∈ B, hypo.
02. 2 ⊢ x ∈ A, hypo.
03. 2 ⊢ set x, set_intro 2.
04. 1, 2 ⊢ x ∈ {x | x ∈ A ∨ x ∈ B}, comp_intro 3 1.
05. 1, 2 ⊢ x ∈ A ∪ B, eq_subst_rev union_eq 4, P u ↔ x ∈ u.
06. 6 ⊢ x ∈ B, hypo.
07. 6 ⊢ set x, set_intro 6.
08. 1, 6 ⊢ x ∈ {x | x ∈ A ∨ x ∈ B}, comp_intro 7 1.
09. 1, 6 ⊢ x ∈ A ∪ B, eq_subst_rev union_eq 8, P u ↔ x ∈ u.
10. 1 ⊢ x ∈ A ∪ B, disj_elim 1 5 9.
union_intro. ⊢ x ∈ A ∨ x ∈ B → x ∈ A ∪ B, subj_intro 10.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.