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

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