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