Theorem df2o3 8461

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 8454	. 2 ⊢ 2o = suc 1o
2		df-suc 6367	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8460	. . . 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 8446  2_oc2o 8447

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 8453  df-2o 8454

This theorem is referenced by:  df2o2  8462  2oex  8465  nlim2  8475  ord2eln012  8482  2oconcl  8488  enpr2d  9045  map2xp  9135  snnen2o  9205  rex2dom  9213  1sdom2dom  9214  cantnflem2  9659  xp2dju  10160  sdom2en01  10286  sadcf  16511  fnpr2o  17611  fnpr2ob  17612  fvprif  17615  xpsfrnel  17616  xpsfeq  17617  xpsle  17633  setcepi  18145  setc2obas  18151  setc2ohom  18152  efgi0  19790  efgi1  19791  vrgpf  19838  vrgpinv  19839  frgpuptinv  19841  frgpup2  19846  frgpup3lem  19847  frgpnabllem1  19943  dmdprdpr  20121  dprdpr  20122  xpstopnlem1  23935  xpstopnlem2  23937  xpsxmetlem  24505  xpsdsval  24507  xpsmet  24508  bdaypw2n0bndlem  28622  onint1  36849  pw2f1ocnv  43656  wepwsolem  43661  omnord1ex  43923  oege2  43926  df3o2  43932  oenord1ex  43934  oenord1  43935  oaomoencom  43936  oenassex  43937  omabs2  43951  omcl3g  43953  clsk1independent  44664  setc1onsubc  50265