Theorem df2o3 8415

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 8408	. 2 ⊢ 2o = suc 1o
2		df-suc 6331	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8414	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4118	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4585	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2763	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2764	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1542   ∪ cun 3901  ∅c0 4287  {csn 4582  {cpr 4584  suc csuc 6327  1_oc1o 8400  2_oc2o 8401

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-dif 3906  df-un 3908  df-nul 4288  df-pr 4585  df-suc 6331  df-1o 8407  df-2o 8408

This theorem is referenced by:  df2o2  8416  2oex  8418  nlim2  8427  ord2eln012  8434  2oconcl  8440  enpr2d  8997  map2xp  9087  snnen2o  9157  rex2dom  9165  1sdom2dom  9166  cantnflem2  9611  xp2dju  10099  sdom2en01  10224  sadcf  16392  fnpr2o  17490  fnpr2ob  17491  fvprif  17494  xpsfrnel  17495  xpsfeq  17496  xpsle  17512  setcepi  18024  setc2obas  18030  setc2ohom  18031  efgi0  19661  efgi1  19662  vrgpf  19709  vrgpinv  19710  frgpuptinv  19712  frgpup2  19717  frgpup3lem  19718  frgpnabllem1  19814  dmdprdpr  19992  dprdpr  19993  xpstopnlem1  23765  xpstopnlem2  23767  xpsxmetlem  24335  xpsdsval  24337  xpsmet  24338  bdaypw2n0bndlem  28471  onint1  36665  pw2f1ocnv  43394  wepwsolem  43399  omnord1ex  43661  oege2  43664  df3o2  43670  oenord1ex  43672  oenord1  43673  oaomoencom  43674  oenassex  43675  omabs2  43689  omcl3g  43691  clsk1independent  44402  setc1onsubc  49961