Theorem bj-elisset

Description: Remove from elisset dependency on ax-ext (and on df-cleq and df-v ). This proof uses only df-clab and df-clel on top of first-order logic. It only requires ax-1--7 and sp . Use bj-elissetv instead when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.)

	Ref	Expression
Assertion	bj-elisset	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		bj-elissetv	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑦 𝑦 = 𝐴 )
2		bj-denotes	⊢ ( ∃ 𝑦 𝑦 = 𝐴 ↔ ∃ 𝑥 𝑥 = 𝐴 )
3	1 2	sylib	⊢ ( 𝐴 ∈ 𝑉 → ∃ 𝑥 𝑥 = 𝐴 )