This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sucel

Description: Membership of a successor in another class. (Contributed by NM, 29-Jun-2004)

Ref Expression
Assertion sucel 
|- ( suc A e. B <-> E. x e. B A. y ( y e. x <-> ( y e. A \/ y = A ) ) )

Proof

Step Hyp Ref Expression
1 risset 
 |-  ( suc A e. B <-> E. x e. B x = suc A )
2 dfcleq 
 |-  ( x = suc A <-> A. y ( y e. x <-> y e. suc A ) )
3 vex 
 |-  y e. _V
4 3 elsuc 
 |-  ( y e. suc A <-> ( y e. A \/ y = A ) )
5 4 bibi2i 
 |-  ( ( y e. x <-> y e. suc A ) <-> ( y e. x <-> ( y e. A \/ y = A ) ) )
6 5 albii 
 |-  ( A. y ( y e. x <-> y e. suc A ) <-> A. y ( y e. x <-> ( y e. A \/ y = A ) ) )
7 2 6 bitri 
 |-  ( x = suc A <-> A. y ( y e. x <-> ( y e. A \/ y = A ) ) )
8 7 rexbii 
 |-  ( E. x e. B x = suc A <-> E. x e. B A. y ( y e. x <-> ( y e. A \/ y = A ) ) )
9 1 8 bitri 
 |-  ( suc A e. B <-> E. x e. B A. y ( y e. x <-> ( y e. A \/ y = A ) ) )