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		ensymb	$$⊢\varnothing \approx \mathrm{suc}B\leftrightarrow \mathrm{suc}B\approx \varnothing$$
3		en0	$$⊢\mathrm{suc}B\approx \varnothing \leftrightarrow \mathrm{suc}B=\varnothing$$
4	2 3	bitri	$$⊢\varnothing \approx \mathrm{suc}B\leftrightarrow \mathrm{suc}B=\varnothing$$
5	1 4	nemtbir	$$⊢\neg \varnothing \approx \mathrm{suc}B$$
6		breq1	$$⊢A=\varnothing \to \left(A\approx \mathrm{suc}B\leftrightarrow \varnothing \approx \mathrm{suc}B\right)$$
7	5 6	mtbiri	$$⊢A=\varnothing \to \neg A\approx \mathrm{suc}B$$
8	7	necon2ai	$$⊢A\approx \mathrm{suc}B\to A\ne \varnothing$$