Metamath Proof Explorer


Theorem clel2

Description: Alternate definition of membership when the member is a set. (Contributed by NM, 18-Aug-1993)

Ref Expression
Hypothesis clel2.1
|- A e. _V
Assertion clel2
|- ( A e. B <-> A. x ( x = A -> x e. B ) )

Proof

Step Hyp Ref Expression
1 clel2.1
 |-  A e. _V
2 clel2g
 |-  ( A e. _V -> ( A e. B <-> A. x ( x = A -> x e. B ) ) )
3 1 2 ax-mp
 |-  ( A e. B <-> A. x ( x = A -> x e. B ) )