Metamath Proof Explorer

Theorem clel3g

Description: An alternate definition of class membership when the class is a set. (Contributed by NM, 13-Aug-2005)

Ref Expression
Assertion clel3g 
|- ( B e. V -> ( A e. B <-> E. x ( x = B /\ A e. x ) ) )

Proof

Step Hyp Ref Expression
1 eleq2 
 |-  ( x = B -> ( A e. x <-> A e. B ) )
2 1 ceqsexgv 
 |-  ( B e. V -> ( E. x ( x = B /\ A e. x ) <-> A e. B ) )
3 2 bicomd 
 |-  ( B e. V -> ( A e. B <-> E. x ( x = B /\ A e. x ) ) )