Theorem df2o3 8530

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 8523	. 2 ⊢ 2o = suc 1o
2		df-suc 6401	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8529	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4187	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4651	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2771	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2772	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1537   ∪ cun 3974  ∅c0 4352  {csn 4648  {cpr 4650  suc csuc 6397  1_oc1o 8515  2_oc2o 8516

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-dif 3979  df-un 3981  df-nul 4353  df-pr 4651  df-suc 6401  df-1o 8522  df-2o 8523

This theorem is referenced by:  df2o2  8531  2oex  8533  nlim2  8546  ord2eln012  8553  2oconcl  8559  enpr2d  9115  map2xp  9213  snnen2o  9300  rex2dom  9309  1sdom2dom  9310  1sdomOLD  9312  cantnflem2  9759  xp2dju  10246  sdom2en01  10371  sadcf  16499  fnpr2o  17617  fnpr2ob  17618  fvprif  17621  xpsfrnel  17622  xpsfeq  17623  xpsle  17639  setcepi  18155  setc2obas  18161  setc2ohom  18162  efgi0  19762  efgi1  19763  vrgpf  19810  vrgpinv  19811  frgpuptinv  19813  frgpup2  19818  frgpup3lem  19819  frgpnabllem1  19915  dmdprdpr  20093  dprdpr  20094  xpstopnlem1  23838  xpstopnlem2  23840  xpsxmetlem  24410  xpsdsval  24412  xpsmet  24413  onint1  36415  pw2f1ocnv  42994  wepwsolem  42999  omnord1ex  43266  oege2  43269  df3o2  43275  oenord1ex  43277  oenord1  43278  oaomoencom  43279  oenassex  43280  omabs2  43294  omcl3g  43296  clsk1independent  44008