Metamath Proof Explorer

Theorem epn0

Description: The membership relation is nonempty. (Contributed by AV, 19-Jun-2022)

Ref Expression
Assertion epn0 
|- _E =/= (/)

Proof

Step Hyp Ref Expression
1 0sn0ep 
 |-  (/) _E { (/) }
2 brne0 
 |-  ( (/) _E { (/) } -> _E =/= (/) )
3 1 2 ax-mp 
 |-  _E =/= (/)