sg_is_inj

Theorem sg_is_inj

Theorem. sg_is_inj
set x → set y → {x} = {y} → x = y

Proof
01. 1 ⊢ set x, hypo.
02. 2 ⊢ set y, hypo.
03. 3 ⊢ {x} = {y}, hypo.
04. ⊢ x = x, eq_refl.
05. 1 ⊢ x ∈ {x}, sg_intro 1 4.
06. 1, 3 ⊢ x ∈ {y}, eq_subst 3 5, P t ↔ x ∈ t.
07. 1, 2, 3 ⊢ x = y, sg_elim 2 6.
sg_is_inj. ⊢ set x → set y → {x} = {y} → x = y,
  subj_intro_iii 7.

Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.