Metamath Proof Explorer

Theorem sucexb

Description: A successor exists iff its class argument exists. (Contributed by NM, 22-Jun-1998)

Ref Expression
Assertion sucexb 
|- ( A e. _V <-> suc A e. _V )

Proof

Step Hyp Ref Expression
1 unexb 
 |-  ( ( A e. _V /\ { A } e. _V ) <-> ( A u. { A } ) e. _V )
2 snex 
 |-  { A } e. _V
3 2 biantru 
 |-  ( A e. _V <-> ( A e. _V /\ { A } e. _V ) )
4 df-suc 
 |-  suc A = ( A u. { A } )
5 4 eleq1i 
 |-  ( suc A e. _V <-> ( A u. { A } ) e. _V )
6 1 3 5 3bitr4i 
 |-  ( A e. _V <-> suc A e. _V )