Theorem df2o3 8445

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 8438	. 2 ⊢ 2o = suc 1o
2		df-suc 6341	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8444	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4130	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4595	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2756	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2757	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1540   ∪ cun 3915  ∅c0 4299  {csn 4592  {cpr 4594  suc csuc 6337  1_oc1o 8430  2_oc2o 8431

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 2702

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 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-dif 3920  df-un 3922  df-nul 4300  df-pr 4595  df-suc 6341  df-1o 8437  df-2o 8438

This theorem is referenced by:  df2o2  8446  2oex  8448  nlim2  8457  ord2eln012  8464  2oconcl  8470  enpr2d  9023  map2xp  9117  snnen2o  9191  rex2dom  9200  1sdom2dom  9201  1sdomOLD  9203  cantnflem2  9650  xp2dju  10137  sdom2en01  10262  sadcf  16430  fnpr2o  17527  fnpr2ob  17528  fvprif  17531  xpsfrnel  17532  xpsfeq  17533  xpsle  17549  setcepi  18057  setc2obas  18063  setc2ohom  18064  efgi0  19657  efgi1  19658  vrgpf  19705  vrgpinv  19706  frgpuptinv  19708  frgpup2  19713  frgpup3lem  19714  frgpnabllem1  19810  dmdprdpr  19988  dprdpr  19989  xpstopnlem1  23703  xpstopnlem2  23705  xpsxmetlem  24274  xpsdsval  24276  xpsmet  24277  onint1  36444  pw2f1ocnv  43033  wepwsolem  43038  omnord1ex  43300  oege2  43303  df3o2  43309  oenord1ex  43311  oenord1  43312  oaomoencom  43313  oenassex  43314  omabs2  43328  omcl3g  43330  clsk1independent  44042  setc1onsubc  49595