Theorem pren2d

Description: A pair of two distinct sets is equinumerous to ordinal two. (Contributed by RP, 21-Oct-2023)

	Ref	Expression
Hypotheses	pren2d.a	|- ( ph -> A e. V )
	pren2d.b	|- ( ph -> B e. W )
	pren2d.aneb	|- ( ph -> A =/= B )
Assertion	pren2d	|- ( ph -> { A , B } ~~ 2o )

Proof

Step	Hyp	Ref	Expression
1		pren2d.a	|- ( ph -> A e. V )
2		pren2d.b	|- ( ph -> B e. W )
3		pren2d.aneb	|- ( ph -> A =/= B )
4	1	elexd	|- ( ph -> A e. _V )
5	2	elexd	|- ( ph -> B e. _V )
6		pren2	|- ( { A , B } ~~ 2o <-> ( A e. _V /\ B e. _V /\ A =/= B ) )
7	4 5 3 6	syl3anbrc	|- ( ph -> { A , B } ~~ 2o )