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\approx \mathrm{suc}B\to A\ne \varnothing$$

Proof

Step	Hyp	Ref	Expression
1		nsuceq0	$$⊢\mathrm{suc}B\ne \varnothing$$
2		en0r	$$⊢\varnothing \approx \mathrm{suc}B\leftrightarrow \mathrm{suc}B=\varnothing$$
3	1 2	nemtbir	$$⊢\neg \varnothing \approx \mathrm{suc}B$$
4		breq1	$$⊢A=\varnothing \to \left(A\approx \mathrm{suc}B\leftrightarrow \varnothing \approx \mathrm{suc}B\right)$$
5	3 4	mtbiri	$$⊢A=\varnothing \to \neg A\approx \mathrm{suc}B$$
6	5	necon2ai	$$⊢A\approx \mathrm{suc}B\to A\ne \varnothing$$