Metamath Proof Explorer


Theorem elsuc2g

Description: Variant of membership in a successor, requiring that B rather than A be a set. (Contributed by NM, 28-Oct-2003)

Ref Expression
Assertion elsuc2g
|- ( B e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )

Proof

Step Hyp Ref Expression
1 df-suc
 |-  suc B = ( B u. { B } )
2 1 eleq2i
 |-  ( A e. suc B <-> A e. ( B u. { B } ) )
3 elun
 |-  ( A e. ( B u. { B } ) <-> ( A e. B \/ A e. { B } ) )
4 elsn2g
 |-  ( B e. V -> ( A e. { B } <-> A = B ) )
5 4 orbi2d
 |-  ( B e. V -> ( ( A e. B \/ A e. { B } ) <-> ( A e. B \/ A = B ) ) )
6 3 5 bitrid
 |-  ( B e. V -> ( A e. ( B u. { B } ) <-> ( A e. B \/ A = B ) ) )
7 2 6 bitrid
 |-  ( B e. V -> ( A e. suc B <-> ( A e. B \/ A = B ) ) )