Metamath Proof Explorer

Theorem elelsuc

Description: Membership in a successor. (Contributed by NM, 20-Jun-1998)

Ref Expression
Assertion elelsuc 
|- ( A e. B -> A e. suc B )

Proof

Step Hyp Ref Expression
1 orc 
 |-  ( A e. B -> ( A e. B \/ A = B ) )
2 elsucg 
 |-  ( A e. B -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )
3 1 2 mpbird 
 |-  ( A e. B -> A e. suc B )