Proof
01. 1 ⊢ set x, hypo.
02. ⊢ x = x, eq_refl.
03. 1 ⊢ x ∈ {x | x = x}, comp_intro 1 2.
04. 1 ⊢ x ∈ UnivCl, eq_subst_rev UnivCl_eq 3, P A ↔ x ∈ A.
UnivCl_intro. ⊢ set x → x ∈ UnivCl, subj_intro 4.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.