Metamath Proof Explorer

Theorem issetlem

Description: Lemma for elisset and isset . (Contributed by NM, 26-May-1993) Extract from the proof of isset . (Revised by WL, 2-Feb-2025)

Ref Expression
Hypothesis issetlem.1 
|- x e. V
Assertion issetlem 
|- ( A e. V <-> E. x x = A )

Proof

Step Hyp Ref Expression
1 issetlem.1 
 |-  x e. V
2 dfclel 
 |-  ( A e. V <-> E. x ( x = A /\ x e. V ) )
3 1 biantru 
 |-  ( x = A <-> ( x = A /\ x e. V ) )
4 3 exbii 
 |-  ( E. x x = A <-> E. x ( x = A /\ x e. V ) )
5 2 4 bitr4i 
 |-  ( A e. V <-> E. x x = A )