Proof
01. 1 ⊢ x ∈ A, hypo.
02. 1 ⊢ set x, set_intro 1.
03. 3 ⊢ u ∈ {x}, hypo.
04. 1, 3 ⊢ u = x, sg_elim 2 3.
05. 1, 3 ⊢ u ∈ A, eq_subst_rev 4 1, P u ↔ u ∈ A.
06. 1 ⊢ u ∈ {x} → u ∈ A, subj_intro 5.
08. 1 ⊢ ∀u. u ∈ {x} → u ∈ A, uq_intro 6.
09. 1 ⊢ {x} ⊆ A, incl_intro 8.
sg_incl_in. ⊢ x ∈ A → {x} ⊆ A, subj_intro 9.
Dependencies
The given proof depends on three axioms:
comp, eq_refl, eq_subst.