Metamath Proof Explorer


Theorem sucprc

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

Ref Expression
Assertion sucprc ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )

Proof

Step Hyp Ref Expression
1 snprc ( ¬ 𝐴 ∈ V ↔ { 𝐴 } = ∅ )
2 1 biimpi ( ¬ 𝐴 ∈ V → { 𝐴 } = ∅ )
3 2 uneq2d ( ¬ 𝐴 ∈ V → ( 𝐴 ∪ { 𝐴 } ) = ( 𝐴 ∪ ∅ ) )
4 df-suc suc 𝐴 = ( 𝐴 ∪ { 𝐴 } )
5 un0 ( 𝐴 ∪ ∅ ) = 𝐴
6 5 eqcomi 𝐴 = ( 𝐴 ∪ ∅ )
7 3 4 6 3eqtr4g ( ¬ 𝐴 ∈ V → suc 𝐴 = 𝐴 )