Theorem df2o3 8405

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 8398	. 2 ⊢ 2o = suc 1o
2		df-suc 6323	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8404	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4116	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4583	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2762	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2763	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1541   ∪ cun 3899  ∅c0 4285  {csn 4580  {cpr 4582  suc csuc 6319  1_oc1o 8390  2_oc2o 8391

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-dif 3904  df-un 3906  df-nul 4286  df-pr 4583  df-suc 6323  df-1o 8397  df-2o 8398

This theorem is referenced by:  df2o2  8406  2oex  8408  nlim2  8417  ord2eln012  8424  2oconcl  8430  enpr2d  8985  map2xp  9075  snnen2o  9145  rex2dom  9153  1sdom2dom  9154  cantnflem2  9599  xp2dju  10087  sdom2en01  10212  sadcf  16380  fnpr2o  17478  fnpr2ob  17479  fvprif  17482  xpsfrnel  17483  xpsfeq  17484  xpsle  17500  setcepi  18012  setc2obas  18018  setc2ohom  18019  efgi0  19649  efgi1  19650  vrgpf  19697  vrgpinv  19698  frgpuptinv  19700  frgpup2  19705  frgpup3lem  19706  frgpnabllem1  19802  dmdprdpr  19980  dprdpr  19981  xpstopnlem1  23753  xpstopnlem2  23755  xpsxmetlem  24323  xpsdsval  24325  xpsmet  24326  bdaypw2n0bndlem  28459  onint1  36643  pw2f1ocnv  43279  wepwsolem  43284  omnord1ex  43546  oege2  43549  df3o2  43555  oenord1ex  43557  oenord1  43558  oaomoencom  43559  oenassex  43560  omabs2  43574  omcl3g  43576  clsk1independent  44287  setc1onsubc  49847