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 𝐴 = 𝐴 )