Metamath Proof Explorer

Theorem pr2cv1

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

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

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 )