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 ensymb 
 |-  ( (/) ~~ suc B <-> suc B ~~ (/) )
3 en0 
 |-  ( suc B ~~ (/) <-> suc B = (/) )
4 2 3 bitri 
 |-  ( (/) ~~ suc B <-> suc B = (/) )
5 1 4 nemtbir 
 |-  -. (/) ~~ suc B
6 breq1 
 |-  ( A = (/) -> ( A ~~ suc B <-> (/) ~~ suc B ) )
7 5 6 mtbiri 
 |-  ( A = (/) -> -. A ~~ suc B )
8 7 necon2ai 
 |-  ( A ~~ suc B -> A =/= (/) )