This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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