Metamath Proof Explorer

Theorem elsuc

Description: Membership in a successor. Exercise 5 of TakeutiZaring p. 17. (Contributed by NM, 15-Sep-2003)

Ref Expression
Hypothesis elsuc.1 
|- A e. _V
Assertion elsuc 
|- ( A e. suc B <-> ( A e. B \/ A = B ) )

Proof

Step Hyp Ref Expression
1 elsuc.1 
 |-  A e. _V
2 elsucg 
 |-  ( A e. _V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )
3 1 2 ax-mp 
 |-  ( A e. suc B <-> ( A e. B \/ A = B ) )