Metamath Proof Explorer

Theorem pr2el2

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 pr2el2 
|- ( { A , B } ~~ 2o -> B e. { A , B } )

Proof

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