Metamath Proof Explorer

Theorem sucprc

Description: A proper class is its own successor. (Contributed by NM, 3-Apr-1995)

Ref Expression
Assertion sucprc 
|- ( -. A e. _V -> suc A = A )

Proof

Step Hyp Ref Expression
1 snprc 
 |-  ( -. A e. _V <-> { A } = (/) )
2 1 biimpi 
 |-  ( -. A e. _V -> { A } = (/) )
3 2 uneq2d 
 |-  ( -. A e. _V -> ( A u. { A } ) = ( A u. (/) ) )
4 df-suc 
 |-  suc A = ( A u. { A } )
5 un0 
 |-  ( A u. (/) ) = A
6 5 eqcomi 
 |-  A = ( A u. (/) )
7 3 4 6 3eqtr4g 
 |-  ( -. A e. _V -> suc A = A )