Metamath Proof Explorer


Theorem bj-elissetALT

Description: Alternate proof of elisset . This is essentially the same proof as seen by inlining bj-denotes and bj-denoteslem . Use elissetv instead when sufficient (in particular when V is substituted for _V ). (Contributed by BJ, 29-Apr-2019) (Proof modification is discouraged.) (New usage is discouraged.)

Ref Expression
Assertion bj-elissetALT ( 𝐴𝑉 → ∃ 𝑥 𝑥 = 𝐴 )

Proof

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