Theorem en2pr

Description: A class is equinumerous to ordinal two iff it is a pair of distinct sets. (Contributed by RP, 11-Oct-2023)

	Ref	Expression
Assertion	en2pr	$$⊢A\approx 2_{𝑜}\leftrightarrow \exists x\exists y\left(A=\left\{x,y\right\}\wedge x\ne y\right)$$

Proof

Step	Hyp	Ref	Expression
1		en2	$$⊢A\approx 2_{𝑜}\to \exists x\exists yA=\left\{x,y\right\}$$
2	1	pm4.71ri	$$⊢A\approx 2_{𝑜}\leftrightarrow \left(\exists x\exists yA=\left\{x,y\right\}\wedge A\approx 2_{𝑜}\right)$$
3		19.41vv	$$⊢\exists x\exists y\left(A=\left\{x,y\right\}\wedge A\approx 2_{𝑜}\right)\leftrightarrow \left(\exists x\exists yA=\left\{x,y\right\}\wedge A\approx 2_{𝑜}\right)$$
4		breq1	$$⊢A=\left\{x,y\right\}\to \left(A\approx 2_{𝑜}\leftrightarrow \left\{x,y\right\}\approx 2_{𝑜}\right)$$
5		pr2ne	$$⊢\left(x\in \mathrm{V}\wedge y\in \mathrm{V}\right)\to \left(\left\{x,y\right\}\approx 2_{𝑜}\leftrightarrow x\ne y\right)$$
6	5	el2v	$$⊢\left\{x,y\right\}\approx 2_{𝑜}\leftrightarrow x\ne y$$
7	4 6	bitrdi	$$⊢A=\left\{x,y\right\}\to \left(A\approx 2_{𝑜}\leftrightarrow x\ne y\right)$$
8	7	pm5.32i	$$⊢\left(A=\left\{x,y\right\}\wedge A\approx 2_{𝑜}\right)\leftrightarrow \left(A=\left\{x,y\right\}\wedge x\ne y\right)$$
9	8	2exbii	$$⊢\exists x\exists y\left(A=\left\{x,y\right\}\wedge A\approx 2_{𝑜}\right)\leftrightarrow \exists x\exists y\left(A=\left\{x,y\right\}\wedge x\ne y\right)$$
10	2 3 9	3bitr2i	$$⊢A\approx 2_{𝑜}\leftrightarrow \exists x\exists y\left(A=\left\{x,y\right\}\wedge x\ne y\right)$$