Theorem df2o3 8403

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 8396	. 2 ⊢ 2o = suc 1o
2		df-suc 6321	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8402	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4114	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4581	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2760	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2761	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1541   ∪ cun 3897  ∅c0 4283  {csn 4578  {cpr 4580  suc csuc 6317  1_oc1o 8388  2_oc2o 8389

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2713  df-cleq 2726  df-clel 2809  df-v 3440  df-dif 3902  df-un 3904  df-nul 4284  df-pr 4581  df-suc 6321  df-1o 8395  df-2o 8396

This theorem is referenced by:  df2o2  8404  2oex  8406  nlim2  8415  ord2eln012  8422  2oconcl  8428  enpr2d  8983  map2xp  9073  snnen2o  9143  rex2dom  9151  1sdom2dom  9152  cantnflem2  9597  xp2dju  10085  sdom2en01  10210  sadcf  16378  fnpr2o  17476  fnpr2ob  17477  fvprif  17480  xpsfrnel  17481  xpsfeq  17482  xpsle  17498  setcepi  18010  setc2obas  18016  setc2ohom  18017  efgi0  19647  efgi1  19648  vrgpf  19695  vrgpinv  19696  frgpuptinv  19698  frgpup2  19703  frgpup3lem  19704  frgpnabllem1  19800  dmdprdpr  19978  dprdpr  19979  xpstopnlem1  23751  xpstopnlem2  23753  xpsxmetlem  24321  xpsdsval  24323  xpsmet  24324  bdaypw2n0s  28420  onint1  36592  pw2f1ocnv  43221  wepwsolem  43226  omnord1ex  43488  oege2  43491  df3o2  43497  oenord1ex  43499  oenord1  43500  oaomoencom  43501  oenassex  43502  omabs2  43516  omcl3g  43518  clsk1independent  44229  setc1onsubc  49789