Metamath Proof Explorer

Theorem clel3

Description: Alternate definition of membership in a set. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis clel3.1 
|- B e. _V
Assertion clel3 
|- ( A e. B <-> E. x ( x = B /\ A e. x ) )

Proof

Step Hyp Ref Expression
1 clel3.1 
 |-  B e. _V
2 clel3g 
 |-  ( B e. _V -> ( A e. B <-> E. x ( x = B /\ A e. x ) ) )
3 1 2 ax-mp 
 |-  ( A e. B <-> E. x ( x = B /\ A e. x ) )