Metamath Proof Explorer


Theorem en3

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

Ref Expression
Assertion en3 A 3 𝑜 x y z A = x y z

Proof

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