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 } ~~ 1o <-> A e. { A } )

Proof

Step Hyp Ref Expression
1 snen1g 
 |-  ( { A } ~~ 1o <-> A e. _V )
2 snidb 
 |-  ( A e. _V <-> A e. { A } )
3 1 2 bitri 
 |-  ( { A } ~~ 1o <-> A e. { A } )