Theorem df2o3 8305

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 8298	. 2 ⊢ 2o = suc 1o
2		df-suc 6272	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8304	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4093	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4564	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2769	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2770	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1539   ∪ cun 3885  ∅c0 4256  {csn 4561  {cpr 4563  suc csuc 6268  1_oc1o 8290  2_oc2o 8291

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3434  df-dif 3890  df-un 3892  df-nul 4257  df-pr 4564  df-suc 6272  df-1o 8297  df-2o 8298

This theorem is referenced by:  df2o2  8306  2oex  8308  nlim2  8320  ord2eln012  8327  2oconcl  8333  map2xp  8934  1sdom  9025  snnen2o  9026  cantnflem2  9448  xp2dju  9932  sdom2en01  10058  sadcf  16160  fnpr2o  17268  fnpr2ob  17269  fvprif  17272  xpsfrnel  17273  xpsfeq  17274  xpsle  17290  setcepi  17803  setc2obas  17809  setc2ohom  17810  efgi0  19326  efgi1  19327  vrgpf  19374  vrgpinv  19375  frgpuptinv  19377  frgpup2  19382  frgpup3lem  19383  frgpnabllem1  19474  dmdprdpr  19652  dprdpr  19653  xpstopnlem1  22960  xpstopnlem2  22962  xpsxmetlem  23532  xpsdsval  23534  xpsmet  23535  onint1  34638  pw2f1ocnv  40859  wepwsolem  40867  df3o2  41634  clsk1independent  41656