Proof
01. 1 ⊢ set y, hypo.
02. ⊢ y = y, eq_refl.
03. 1 ⊢ y ∈ {y}, sg_intro 1 2.
04. ⊢ {y} ⊆ {x, y}, union_incl_right.
05. 1 ⊢ y ∈ {x, y}, incl_elim 4 3.
in22. ⊢ set y → y ∈ {x, y}, subj_intro 5.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.