Theorem df2o3 8478

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 8471	. 2 ⊢ 2o = suc 1o
2		df-suc 6371	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8477	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4160	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4632	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2761	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2762	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1539   ∪ cun 3947  ∅c0 4323  {csn 4629  {cpr 4631  suc csuc 6367  1_oc1o 8463  2_oc2o 8464

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 1911  ax-6 1969  ax-7 2009  ax-8 2106  ax-9 2114  ax-ext 2701

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 844  df-tru 1542  df-fal 1552  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2722  df-clel 2808  df-v 3474  df-dif 3952  df-un 3954  df-nul 4324  df-pr 4632  df-suc 6371  df-1o 8470  df-2o 8471

This theorem is referenced by:  df2o2  8479  2oex  8481  nlim2  8494  ord2eln012  8501  2oconcl  8507  enpr2d  9053  map2xp  9151  snnen2o  9241  rex2dom  9250  1sdom2dom  9251  1sdomOLD  9253  cantnflem2  9689  xp2dju  10175  sdom2en01  10301  sadcf  16400  fnpr2o  17509  fnpr2ob  17510  fvprif  17513  xpsfrnel  17514  xpsfeq  17515  xpsle  17531  setcepi  18044  setc2obas  18050  setc2ohom  18051  efgi0  19631  efgi1  19632  vrgpf  19679  vrgpinv  19680  frgpuptinv  19682  frgpup2  19687  frgpup3lem  19688  frgpnabllem1  19784  dmdprdpr  19962  dprdpr  19963  xpstopnlem1  23535  xpstopnlem2  23537  xpsxmetlem  24107  xpsdsval  24109  xpsmet  24110  onint1  35639  pw2f1ocnv  42080  wepwsolem  42088  omnord1ex  42358  oege2  42361  df3o2  42367  oenord1ex  42369  oenord1  42370  oaomoencom  42371  oenassex  42372  omabs2  42386  omcl3g  42388  clsk1independent  43101