Theorem df2o3 8413

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 8406	. 2 ⊢ 2o = suc 1o
2		df-suc 6329	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8412	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4104	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4570	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2762	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2763	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1542   ∪ cun 3887  ∅c0 4273  {csn 4567  {cpr 4569  suc csuc 6325  1_oc1o 8398  2_oc2o 8399

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-dif 3892  df-un 3894  df-nul 4274  df-pr 4570  df-suc 6329  df-1o 8405  df-2o 8406

This theorem is referenced by:  df2o2  8414  2oex  8416  nlim2  8425  ord2eln012  8432  2oconcl  8438  enpr2d  8995  map2xp  9085  snnen2o  9155  rex2dom  9163  1sdom2dom  9164  cantnflem2  9611  xp2dju  10099  sdom2en01  10224  sadcf  16422  fnpr2o  17521  fnpr2ob  17522  fvprif  17525  xpsfrnel  17526  xpsfeq  17527  xpsle  17543  setcepi  18055  setc2obas  18061  setc2ohom  18062  efgi0  19695  efgi1  19696  vrgpf  19743  vrgpinv  19744  frgpuptinv  19746  frgpup2  19751  frgpup3lem  19752  frgpnabllem1  19848  dmdprdpr  20026  dprdpr  20027  xpstopnlem1  23774  xpstopnlem2  23776  xpsxmetlem  24344  xpsdsval  24346  xpsmet  24347  bdaypw2n0bndlem  28455  onint1  36631  pw2f1ocnv  43465  wepwsolem  43470  omnord1ex  43732  oege2  43735  df3o2  43741  oenord1ex  43743  oenord1  43744  oaomoencom  43745  oenassex  43746  omabs2  43760  omcl3g  43762  clsk1independent  44473  setc1onsubc  50077