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 6352	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8444	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4117	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4585	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2788	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2789	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1560   ∪ cun 3902  ∅c0 4285  {csn 4582  {cpr 4584  suc csuc 6348  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 1815  ax-4 1829  ax-5 1930  ax-6 1987  ax-7 2028  ax-8 2144  ax-9 2152  ax-ext 2734

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1563  df-fal 1573  df-ex 1800  df-sb 2091  df-clab 2741  df-cleq 2754  df-clel 2837  df-v 3456  df-dif 3907  df-un 3909  df-nul 4286  df-pr 4585  df-suc 6352  df-1o 8437  df-2o 8438

This theorem is referenced by:  df2o2  8446  2oex  8449  nlim2  8459  ord2eln012  8466  2oconcl  8472  enpr2d  9029  map2xp  9119  snnen2o  9189  rex2dom  9197  1sdom2dom  9198  cantnflem2  9645  xp2dju  10133  sdom2en01  10259  sadcf  16487  fnpr2o  17587  fnpr2ob  17588  fvprif  17591  xpsfrnel  17592  xpsfeq  17593  xpsle  17609  setcepi  18121  setc2obas  18127  setc2ohom  18128  efgi0  19760  efgi1  19761  vrgpf  19808  vrgpinv  19809  frgpuptinv  19811  frgpup2  19816  frgpup3lem  19817  frgpnabllem1  19913  dmdprdpr  20091  dprdpr  20092  xpstopnlem1  23869  xpstopnlem2  23871  xpsxmetlem  24439  xpsdsval  24441  xpsmet  24442  bdaypw2n0bndlem  28556  onint1  36809  pw2f1ocnv  43614  wepwsolem  43619  omnord1ex  43881  oege2  43884  df3o2  43890  oenord1ex  43892  oenord1  43893  oaomoencom  43894  oenassex  43895  omabs2  43909  omcl3g  43911  clsk1independent  44622  setc1onsubc  50223