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 ⊢ M ∈ ω ∧ A ≈ suc ⁡ M ∧ X ∈ A → A ∖ X ≈ M

Proof

Step Hyp Ref Expression
1 nnon ⊢ M ∈ ω → M ∈ On
2 dif1en ⊢ M ∈ On ∧ A ≈ suc ⁡ M ∧ X ∈ A → A ∖ X ≈ M
3 1 2 syl3an1 ⊢ M ∈ ω ∧ A ≈ suc ⁡ M ∧ X ∈ A → A ∖ X ≈ M