Theorem set_from_sg

Proof
01. 1 ⊢ ¬set x, hypo.
02. 1 ⊢ {x} = UnivCl, sg_of_proper_class 1.
03. 1 ⊢ ¬set {x}, eq_subst_rev 2 UnivCl_is_proper, P u ↔ ¬set u.
04. ⊢ ¬set x → ¬set {x}, subj_intro 3.
set_from_sg. ⊢ set {x} → set x, contraposition_rev 4.

Dependencies
The given proof depends on seven axioms:
comp, efq, eq_refl, eq_subst, ext, lem, subset.