Metamath Proof Explorer


Theorem snen1el

Description: A singleton is equinumerous to ordinal one if its content is an element of it. (Contributed by RP, 8-Oct-2023)

Ref Expression
Assertion snen1el A 1 𝑜 A A

Proof

Step Hyp Ref Expression
1 snen1g A 1 𝑜 A V
2 snidb A V A A
3 1 2 bitri A 1 𝑜 A A