Metamath Proof Explorer

Theorem 0el

Description: Membership of the empty set in another class. (Contributed by NM, 29-Jun-2004)

Ref Expression
Assertion 0el 
|- ( (/) e. A <-> E. x e. A A. y -. y e. x )

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( (/) e. A <-> E. x e. A x = (/) )
2 eq0 
 |-  ( x = (/) <-> A. y -. y e. x )
3 2 rexbii 
 |-  ( E. x e. A x = (/) <-> E. x e. A A. y -. y e. x )
4 1 3 bitri 
 |-  ( (/) e. A <-> E. x e. A A. y -. y e. x )