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	|- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )

Proof

Step	Hyp	Ref	Expression
1		nnon	|- ( M e. _om -> M e. On )
2		dif1en	|- ( ( M e. On /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )
3	1 2	syl3an1	|- ( ( M e. _om /\ A ~~ suc M /\ X e. A ) -> ( A \ { X } ) ~~ M )