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		ensymb	⊢ ( ∅ ≈ suc 𝐵 ↔ suc 𝐵 ≈ ∅ )
3		en0	⊢ ( suc 𝐵 ≈ ∅ ↔ suc 𝐵 = ∅ )
4	2 3	bitri	⊢ ( ∅ ≈ suc 𝐵 ↔ suc 𝐵 = ∅ )
5	1 4	nemtbir	⊢ ¬ ∅ ≈ suc 𝐵
6		breq1	⊢ ( 𝐴 = ∅ → ( 𝐴 ≈ suc 𝐵 ↔ ∅ ≈ suc 𝐵 ) )
7	5 6	mtbiri	⊢ ( 𝐴 = ∅ → ¬ 𝐴 ≈ suc 𝐵 )
8	7	necon2ai	⊢ ( 𝐴 ≈ suc 𝐵 → 𝐴 ≠ ∅ )