Theorem df2o3 8464

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 8457	. 2 ⊢ 2o = suc 1o
2		df-suc 6363	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8463	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4111	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4587	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2786	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2787	1 ⊢ 2o = {∅, 1o}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897  ∅c0 4279  {csn 4584  {cpr 4586  suc csuc 6359  1_oc1o 8449  2_oc2o 8450

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-dif 3902  df-un 3904  df-nul 4280  df-pr 4587  df-suc 6363  df-1o 8456  df-2o 8457

This theorem is used by:  df2o2  8465  2oex  8468  nlim2  8478  ord2eln012  8485  2oconcl  8491  enpr2d  9056  map2xp  9146  snnen2o  9216  rex2dom  9224  1sdom2dom  9225  cantnflem2  9670  xp2dju  10180  sdom2en01  10305  sadcf  16544  fnpr2o  17644  fnpr2ob  17645  fvprif  17648  xpsfrnel  17649  xpsfeq  17650  xpsle  17666  setcepi  18178  setc2obas  18184  setc2ohom  18185  efgi0  19848  efgi1  19849  vrgpf  19896  vrgpinv  19897  frgpuptinv  19899  frgpup2  19904  frgpup3lem  19905  frgpnabllem1  20001  dmdprdpr  20179  dprdpr  20180  xpstopnlem1  24036  xpstopnlem2  24038  xpsxmetlem  24606  xpsdsval  24608  xpsmet  24609  bdaypw2n0bndlem  28729  onint1  37069  pw2f1ocnv  43879  wepwsolem  43884  omnord1ex  44146  oege2  44149  df3o2  44155  oenord1ex  44157  oenord1  44158  oaomoencom  44159  oenassex  44160  omabs2  44174  omcl3g  44176  clsk1independent  44887  setc1onsubc  50529