Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ set y, hypo.
03. 1, 2 ⊢ set {x, y}, pairing 1 2.
04. ⊢ set {x, y} → set (⋃{x, y}), union.
05. 1, 2 ⊢ set (⋃{x, y}), subj_elim 4 3.
06. 1, 2 ⊢ set x ∧ set y, conj_intro 1 2.
07. 1, 2 ⊢ ⋃{x, y} = x ∪ y, Union_pair_set 6.
08. 1, 2 ⊢ set (x ∪ y), eq_subst 7 5, P u ↔ set u.
set_union. ⊢ set x → set y → set (x ∪ y), subj_intro_ii 8.
Dependencies
The given proof depends on six axioms:
comp, eq_refl, eq_subst, ext, pairing, union.