Metamath Proof Explorer


Theorem pr2cv2

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 pr2cv2 AB2𝑜BV

Proof

Step Hyp Ref Expression
1 pr2cv AB2𝑜AVBV
2 1 simprd AB2𝑜BV