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 V A suc B A B A = B

Proof

Step Hyp Ref Expression
1 df-suc suc B = B B
2 1 eleq2i A suc B A B B
3 elun A B B A B A B
4 elsn2g B V A B A = B
5 4 orbi2d B V A B A B A B A = B
6 3 5 syl5bb B V A B B A B A = B
7 2 6 syl5bb B V A suc B A B A = B