Metamath Proof Explorer

Theorem bnj923

Description: First-order logic and set theory. (Contributed by Jonathan Ben-Naim, 3-Jun-2011) (New usage is discouraged.)

Ref Expression
Hypothesis bnj923.1 
|- D = ( _om \ { (/) } )
Assertion bnj923 
|- ( n e. D -> n e. _om )

Proof

Step Hyp Ref Expression
1 bnj923.1 
 |-  D = ( _om \ { (/) } )
2 eldifi 
 |-  ( n e. ( _om \ { (/) } ) -> n e. _om )
3 2 1 eleq2s 
 |-  ( n e. D -> n e. _om )