Theorem dif1ennn

Description: If a set A is equinumerous to the successor of a natural number M , then A with an element removed is equinumerous to M . See also dif1ennnALT . (Contributed by BTernaryTau, 6-Jan-2025)

	Ref	Expression
Assertion	dif1ennn	$$⊢\left(M\in \mathrm{\omega }\wedge A\approx \mathrm{suc}M\wedge X\in A\right)\to \left(A\setminus \left\{X\right\}\right)\approx M$$

Proof

Step	Hyp	Ref	Expression
1		nnon	$$⊢M\in \mathrm{\omega }\to M\in \mathrm{On}$$
2		dif1en	$$⊢\left(M\in \mathrm{On}\wedge A\approx \mathrm{suc}M\wedge X\in A\right)\to \left(A\setminus \left\{X\right\}\right)\approx M$$
3	1 2	syl3an1	$$⊢\left(M\in \mathrm{\omega }\wedge A\approx \mathrm{suc}M\wedge X\in A\right)\to \left(A\setminus \left\{X\right\}\right)\approx M$$