Metamath Proof Explorer


Theorem en2

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

Ref Expression
Assertion en2 A 2 𝑜 x y A = x y

Proof

Step Hyp Ref Expression
1 1on 1 𝑜 On
2 1 onordi Ord 1 𝑜
3 df-2o 2 𝑜 = suc 1 𝑜
4 en1 A x 1 𝑜 y A x = y
5 4 biimpi A x 1 𝑜 y A x = y
6 df-pr x y = x y
7 6 enp1ilem x A A x = y A = x y
8 7 eximdv x A y A x = y y A = x y
9 2 3 5 8 enp1i A 2 𝑜 x y A = x y