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	|- ( ph -> A e. C )
	enpr2d.2	|- ( ph -> B e. D )
	enpr2d.3	|- ( ph -> -. A = B )
Assertion	enpr2d	|- ( ph -> { A , B } ~~ 2o )

Proof

Step	Hyp	Ref	Expression
1		enpr2d.1	|- ( ph -> A e. C )
2		enpr2d.2	|- ( ph -> B e. D )
3		enpr2d.3	|- ( ph -> -. A = B )
4		0ex	|- (/) e. _V
5	4	a1i	|- ( ph -> (/) e. _V )
6		1oex	|- 1o e. _V
7	6	a1i	|- ( ph -> 1o e. _V )
8	3	neqned	|- ( ph -> A =/= B )
9		1n0	|- 1o =/= (/)
10	9	necomi	|- (/) =/= 1o
11	10	a1i	|- ( ph -> (/) =/= 1o )
12	1 2 5 7 8 11	en2prd	|- ( ph -> { A , B } ~~ { (/) , 1o } )
13		df2o3	|- 2o = { (/) , 1o }
14	12 13	breqtrrdi	|- ( ph -> { A , B } ~~ 2o )