Theorem df2o3 8474

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

Syntax hints:   = wceq 1542   ∪ cun 3947  ∅c0 4323  {csn 4629  {cpr 4631  suc csuc 6367  1_oc1o 8459  2_oc2o 8460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-dif 3952  df-un 3954  df-nul 4324  df-pr 4632  df-suc 6371  df-1o 8466  df-2o 8467

This theorem is referenced by:  df2o2  8475  2oex  8477  nlim2  8490  ord2eln012  8497  2oconcl  8503  enpr2d  9049  map2xp  9147  snnen2o  9237  rex2dom  9246  1sdom2dom  9247  1sdomOLD  9249  cantnflem2  9685  xp2dju  10171  sdom2en01  10297  sadcf  16394  fnpr2o  17503  fnpr2ob  17504  fvprif  17507  xpsfrnel  17508  xpsfeq  17509  xpsle  17525  setcepi  18038  setc2obas  18044  setc2ohom  18045  efgi0  19588  efgi1  19589  vrgpf  19636  vrgpinv  19637  frgpuptinv  19639  frgpup2  19644  frgpup3lem  19645  frgpnabllem1  19741  dmdprdpr  19919  dprdpr  19920  xpstopnlem1  23313  xpstopnlem2  23315  xpsxmetlem  23885  xpsdsval  23887  xpsmet  23888  onint1  35334  pw2f1ocnv  41776  wepwsolem  41784  omnord1ex  42054  oege2  42057  df3o2  42063  oenord1ex  42065  oenord1  42066  oaomoencom  42067  oenassex  42068  omabs2  42082  omcl3g  42084  clsk1independent  42797