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	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to A\in \mathrm{V}$$

Proof

Step	Hyp	Ref	Expression
1		pr2cv	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to \left(A\in \mathrm{V}\wedge B\in \mathrm{V}\right)$$
2	1	simpld	$$⊢\left\{A,B\right\}\approx 2_{𝑜}\to A\in \mathrm{V}$$