Proof
01. 1 ⊢ univ U, hypo.
02. 2 ⊢ x ∈ U, hypo.
03. 2 ⊢ set x, set_intro 2.
04. 2 ⊢ {x} ⊆ power x, sg_incl_in_power 3.
05. 2 ⊢ set {x}, set_sg 3.
06. 2 ⊢ {x} ∈ power (power x), power_intro 5 4.
07. 1, 2 ⊢ power x ∈ U, univ_closed_power 1 2.
08. 1, 2 ⊢ power (power x) ∈ U, univ_closed_power 1 7.
09. 1, 2 ⊢ power (power x) ⊆ U, univ_trans 1 8.
10. 1, 2 ⊢ {x} ∈ U, incl_elim 9 6.
univ_closed_sg. ⊢ univ U → x ∈ U → {x} ∈ U, subj_intro_ii 10.
Dependencies
The given proof depends on five axioms:
comp, eq_refl, eq_subst, ext, pairing.