Theorem enpr2d

Description: A pair with distinct elements is equinumerous to ordinal two. (Contributed by Rohan Ridenour, 3-Aug-2023) Avoid ax-un . (Revised by BTernaryTau, 23-Dec-2024)

	Ref	Expression
Hypotheses	enpr2d.1	$$⊢\phi \to A\in C$$
	enpr2d.2	$$⊢\phi \to B\in D$$
	enpr2d.3	$$⊢\phi \to \neg A=B$$
Assertion	enpr2d	$$⊢\phi \to \left\{A,B\right\}\approx 2_{𝑜}$$

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	$$⊢\phi \to A\in C$$
2		enpr2d.2	$$⊢\phi \to B\in D$$
3		enpr2d.3	$$⊢\phi \to \neg A=B$$
4		0ex	$$⊢\varnothing \in \mathrm{V}$$
5	4	a1i	$$⊢\phi \to \varnothing \in \mathrm{V}$$
6		1oex	$$⊢1_{𝑜}\in \mathrm{V}$$
7	6	a1i	$$⊢\phi \to 1_{𝑜}\in \mathrm{V}$$
8	3	neqned	$$⊢\phi \to A\ne B$$
9		1n0	$$⊢1_{𝑜}\ne \varnothing$$
10	9	necomi	$$⊢\varnothing \ne 1_{𝑜}$$
11	10	a1i	$$⊢\phi \to \varnothing \ne 1_{𝑜}$$
12	1 2 5 7 8 11	en2prd	$$⊢\phi \to \left\{A,B\right\}\approx \left\{\varnothing ,1_{𝑜}\right\}$$
13		df2o3	$$⊢2_{𝑜}=\left\{\varnothing ,1_{𝑜}\right\}$$
14	12 13	breqtrrdi	$$⊢\phi \to \left\{A,B\right\}\approx 2_{𝑜}$$