Metamath Proof Explorer

Theorem bnj219

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

Ref Expression
Assertion bnj219 
|- ( n = suc m -> m _E n )

Proof

Step Hyp Ref Expression
1 vex 
 |-  m e. _V
2 1 bnj216 
 |-  ( n = suc m -> m e. n )
3 epel 
 |-  ( m _E n <-> m e. n )
4 2 3 sylibr 
 |-  ( n = suc m -> m _E n )