Theorem df2o3 8460

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 8453	. 2 ⊢ 2o = suc 1o
2		df-suc 6367	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8459	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4126	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4597	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2795	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2796	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1567   ∪ cun 3911  ∅c0 4294  {csn 4594  {cpr 4596  suc csuc 6363  1_oc1o 8445  2_oc2o 8446

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-dif 3916  df-un 3918  df-nul 4295  df-pr 4597  df-suc 6367  df-1o 8452  df-2o 8453

This theorem is referenced by:  df2o2  8461  2oex  8464  nlim2  8474  ord2eln012  8481  2oconcl  8487  enpr2d  9044  map2xp  9134  snnen2o  9204  rex2dom  9212  1sdom2dom  9213  cantnflem2  9658  xp2dju  10159  sdom2en01  10285  sadcf  16510  fnpr2o  17610  fnpr2ob  17611  fvprif  17614  xpsfrnel  17615  xpsfeq  17616  xpsle  17632  setcepi  18144  setc2obas  18150  setc2ohom  18151  efgi0  19789  efgi1  19790  vrgpf  19837  vrgpinv  19838  frgpuptinv  19840  frgpup2  19845  frgpup3lem  19846  frgpnabllem1  19942  dmdprdpr  20120  dprdpr  20121  xpstopnlem1  23934  xpstopnlem2  23936  xpsxmetlem  24504  xpsdsval  24506  xpsmet  24507  bdaypw2n0bndlem  28621  onint1  36848  pw2f1ocnv  43655  wepwsolem  43660  omnord1ex  43922  oege2  43925  df3o2  43931  oenord1ex  43933  oenord1  43934  oaomoencom  43935  oenassex  43936  omabs2  43950  omcl3g  43952  clsk1independent  44663  setc1onsubc  50264