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