Theorem df2o3 8493

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 8486	. 2 ⊢ 2o = suc 1o
2		df-suc 6363	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8492	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4144	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4609	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2762	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2763	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1540   ∪ cun 3929  ∅c0 4313  {csn 4606  {cpr 4608  suc csuc 6359  1_oc1o 8478  2_oc2o 8479

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-dif 3934  df-un 3936  df-nul 4314  df-pr 4609  df-suc 6363  df-1o 8485  df-2o 8486

This theorem is referenced by:  df2o2  8494  2oex  8496  nlim2  8507  ord2eln012  8514  2oconcl  8520  enpr2d  9068  map2xp  9166  snnen2o  9250  rex2dom  9259  1sdom2dom  9260  1sdomOLD  9262  cantnflem2  9709  xp2dju  10196  sdom2en01  10321  sadcf  16477  fnpr2o  17576  fnpr2ob  17577  fvprif  17580  xpsfrnel  17581  xpsfeq  17582  xpsle  17598  setcepi  18106  setc2obas  18112  setc2ohom  18113  efgi0  19706  efgi1  19707  vrgpf  19754  vrgpinv  19755  frgpuptinv  19757  frgpup2  19762  frgpup3lem  19763  frgpnabllem1  19859  dmdprdpr  20037  dprdpr  20038  xpstopnlem1  23752  xpstopnlem2  23754  xpsxmetlem  24323  xpsdsval  24325  xpsmet  24326  onint1  36472  pw2f1ocnv  43028  wepwsolem  43033  omnord1ex  43295  oege2  43298  df3o2  43304  oenord1ex  43306  oenord1  43307  oaomoencom  43308  oenassex  43309  omabs2  43323  omcl3g  43325  clsk1independent  44037  setc1onsubc  49446