Metamath Proof Explorer

Theorem pr2el1

Description: If an unordered pair is equinumerous to ordinal two, then a part is a member. (Contributed by RP, 21-Oct-2023)

Ref Expression
Assertion pr2el1 
|- ( { A , B } ~~ 2o -> A e. { A , B } )

Proof

Step Hyp Ref Expression
1 pr2cv 
 |-  ( { A , B } ~~ 2o -> ( A e. _V /\ B e. _V ) )
2 1 simpld 
 |-  ( { A , B } ~~ 2o -> A e. _V )
3 prid1g 
 |-  ( A e. _V -> A e. { A , B } )
4 2 3 syl 
 |-  ( { A , B } ~~ 2o -> A e. { A , B } )