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	⊢ ( 𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅ )

Proof

Step	Hyp	Ref	Expression
1		nsuceq0	⊢ suc 𝐵 ≠ ∅
2		en0r	⊢ ( ∅ ≈ suc 𝐵 ↔ suc 𝐵 = ∅ )
3	1 2	nemtbir	⊢ ¬ ∅ ≈ suc 𝐵
4		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≈ suc 𝐵 ↔ ∅ ≈ suc 𝐵 ) )
5	3 4	mtbiri	⊢ ( 𝐴 = ∅ → ¬ 𝐴 ≈ suc 𝐵 )
6	5	necon2ai	⊢ ( 𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅ )