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	⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )

Proof

Step	Hyp	Ref	Expression
1		nnon	⊢ ( 𝑀 ∈ ω → 𝑀 ∈ On )
2		dif1en	⊢ ( ( 𝑀 ∈ On ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )
3	1 2	syl3an1	⊢ ( ( 𝑀 ∈ ω ∧ 𝐴 ≈ suc 𝑀 ∧ 𝑋 ∈ 𝐴 ) → ( 𝐴 ∖ { 𝑋 } ) ≈ 𝑀 )