Metamath Proof Explorer

Theorem ensucne0

Description: A class equinumerous to a successor is never empty. (Contributed by RP, 11-Nov-2023) (Proof shortened by SN, 16-Nov-2023)

Ref Expression
Assertion ensucne0 
|- ( A ~~ suc B -> A =/= (/) )

Proof

Step Hyp Ref Expression
1 nsuceq0 
 |-  suc B =/= (/)
2 en0r 
 |-  ( (/) ~~ suc B <-> suc B = (/) )
3 1 2 nemtbir 
 |-  -. (/) ~~ suc B
4 breq1 
 |-  ( A = (/) -> ( A ~~ suc B <-> (/) ~~ suc B ) )
5 3 4 mtbiri 
 |-  ( A = (/) -> -. A ~~ suc B )
6 5 necon2ai 
 |-  ( A ~~ suc B -> A =/= (/) )