Theorem en2

Description: A set equinumerous to ordinal 2 is a pair. (Contributed by Mario Carneiro, 5-Jan-2016)

	Ref	Expression
Assertion	en2	|- ( A ~~ 2o -> E. x E. y A = { x , y } )

Proof

Step	Hyp	Ref	Expression
1		1on	|- 1o e. On
2	1	onordi	|- Ord 1o
3		df-2o	|- 2o = suc 1o
4		en1	|- ( ( A \ { x } ) ~~ 1o <-> E. y ( A \ { x } ) = { y } )
5	4	biimpi	|- ( ( A \ { x } ) ~~ 1o -> E. y ( A \ { x } ) = { y } )
6		df-pr	|- { x , y } = ( { x } u. { y } )
7	6	enp1ilem	|- ( x e. A -> ( ( A \ { x } ) = { y } -> A = { x , y } ) )
8	7	eximdv	|- ( x e. A -> ( E. y ( A \ { x } ) = { y } -> E. y A = { x , y } ) )
9	2 3 5 8	enp1i	|- ( A ~~ 2o -> E. x E. y A = { x , y } )