Theorem df2o3 8419

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 8412	. 2 ⊢ 2o = suc 1o
2		df-suc 6326	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8418	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4123	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4588	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2755	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2756	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1540   ∪ cun 3909  ∅c0 4292  {csn 4585  {cpr 4587  suc csuc 6322  1_oc1o 8404  2_oc2o 8405

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 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-dif 3914  df-un 3916  df-nul 4293  df-pr 4588  df-suc 6326  df-1o 8411  df-2o 8412

This theorem is referenced by:  df2o2  8420  2oex  8422  nlim2  8431  ord2eln012  8438  2oconcl  8444  enpr2d  8997  map2xp  9088  snnen2o  9161  rex2dom  9169  1sdom2dom  9170  1sdomOLD  9172  cantnflem2  9619  xp2dju  10106  sdom2en01  10231  sadcf  16399  fnpr2o  17496  fnpr2ob  17497  fvprif  17500  xpsfrnel  17501  xpsfeq  17502  xpsle  17518  setcepi  18026  setc2obas  18032  setc2ohom  18033  efgi0  19626  efgi1  19627  vrgpf  19674  vrgpinv  19675  frgpuptinv  19677  frgpup2  19682  frgpup3lem  19683  frgpnabllem1  19779  dmdprdpr  19957  dprdpr  19958  xpstopnlem1  23672  xpstopnlem2  23674  xpsxmetlem  24243  xpsdsval  24245  xpsmet  24246  onint1  36410  pw2f1ocnv  42999  wepwsolem  43004  omnord1ex  43266  oege2  43269  df3o2  43275  oenord1ex  43277  oenord1  43278  oaomoencom  43279  oenassex  43280  omabs2  43294  omcl3g  43296  clsk1independent  44008  setc1onsubc  49564