Theorem df2o3 8442

Description: Expanded value of the ordinal number 2. (Contributed by Mario Carneiro, 14-Aug-2015.)

Assertion

Ref	Expression
df2o3	⊢ 2o = {∅, 1o}

Proof of Theorem df2o3

Step	Hyp	Ref	Expression
1		df-2o 8435	. 2 ⊢ 2o = suc 1o
2		df-suc 6338	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8441	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4127	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4592	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2755	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2756	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1540   ∪ cun 3912  ∅c0 4296  {csn 4589  {cpr 4591  suc csuc 6334  1_oc1o 8427  2_oc2o 8428

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-dif 3917  df-un 3919  df-nul 4297  df-pr 4592  df-suc 6338  df-1o 8434  df-2o 8435

This theorem is referenced by:  df2o2  8443  2oex  8445  nlim2  8454  ord2eln012  8461  2oconcl  8467  enpr2d  9020  map2xp  9111  snnen2o  9184  rex2dom  9193  1sdom2dom  9194  1sdomOLD  9196  cantnflem2  9643  xp2dju  10130  sdom2en01  10255  sadcf  16423  fnpr2o  17520  fnpr2ob  17521  fvprif  17524  xpsfrnel  17525  xpsfeq  17526  xpsle  17542  setcepi  18050  setc2obas  18056  setc2ohom  18057  efgi0  19650  efgi1  19651  vrgpf  19698  vrgpinv  19699  frgpuptinv  19701  frgpup2  19706  frgpup3lem  19707  frgpnabllem1  19803  dmdprdpr  19981  dprdpr  19982  xpstopnlem1  23696  xpstopnlem2  23698  xpsxmetlem  24267  xpsdsval  24269  xpsmet  24270  onint1  36437  pw2f1ocnv  43026  wepwsolem  43031  omnord1ex  43293  oege2  43296  df3o2  43302  oenord1ex  43304  oenord1  43305  oaomoencom  43306  oenassex  43307  omabs2  43321  omcl3g  43323  clsk1independent  44035  setc1onsubc  49591