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 ~~ 2o <-> E. x E. y ( A = { x , y } /\ x =/= y ) )

Proof

Step	Hyp	Ref	Expression
1		en2	|- ( A ~~ 2o -> E. x E. y A = { x , y } )
2	1	pm4.71ri	|- ( A ~~ 2o <-> ( E. x E. y A = { x , y } /\ A ~~ 2o ) )
3		19.41vv	|- ( E. x E. y ( A = { x , y } /\ A ~~ 2o ) <-> ( E. x E. y A = { x , y } /\ A ~~ 2o ) )
4		breq1	|- ( A = { x , y } -> ( A ~~ 2o <-> { x , y } ~~ 2o ) )
5		pr2ne	|- ( ( x e. _V /\ y e. _V ) -> ( { x , y } ~~ 2o <-> x =/= y ) )
6	5	el2v	|- ( { x , y } ~~ 2o <-> x =/= y )
7	4 6	bitrdi	|- ( A = { x , y } -> ( A ~~ 2o <-> x =/= y ) )
8	7	pm5.32i	|- ( ( A = { x , y } /\ A ~~ 2o ) <-> ( A = { x , y } /\ x =/= y ) )
9	8	2exbii	|- ( E. x E. y ( A = { x , y } /\ A ~~ 2o ) <-> E. x E. y ( A = { x , y } /\ x =/= y ) )
10	2 3 9	3bitr2i	|- ( A ~~ 2o <-> E. x E. y ( A = { x , y } /\ x =/= y ) )