Proof
01. 1 ⊢ ¬set A, hypo.
02. 2 ⊢ set A, hypo.
03. 1, 2 ⊢ ⊥, neg_elim 1 2.
04. 1, 2 ⊢ x = A, efq 3.
05. 1 ⊢ set A → x = A, subj_intro 4.
06. 6 ⊢ x ∈ UnivCl, hypo.
07. 6 ⊢ set x, set_intro 6.
08. 1, 6 ⊢ x ∈ {x | set A → x = A}, comp_intro 7 5.
09. ⊢ {A} = {x | set A → x = A}, sg_eq.
10. 1, 6 ⊢ x ∈ {A}, eq_subst_rev 9 8, P u ↔ x ∈ u.
11. 1 ⊢ x ∈ UnivCl → x ∈ {A}, subj_intro 10.
12. 1 ⊢ ∀x. x ∈ UnivCl → x ∈ {A}, uq_intro 11.
13. 1 ⊢ UnivCl ⊆ {A}, incl_intro 12.
14. ⊢ {A} ⊆ UnivCl, UnivCl_is_greatest.
15. 1 ⊢ {A} = UnivCl, incl_antisym 14 13.
sg_of_proper_class. ⊢ ¬set A → {A} = UnivCl, subj_intro 15.
Dependencies
The given proof depends on five axioms:
comp, efq, eq_refl, eq_subst, ext.