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  18030  setc2obas  18036  setc2ohom  18037  efgi0  19634  efgi1  19635  vrgpf  19682  vrgpinv  19683  frgpuptinv  19685  frgpup2  19690  frgpup3lem  19691  frgpnabllem1  19787  dmdprdpr  19965  dprdpr  19966  xpstopnlem1  23729  xpstopnlem2  23731  xpsxmetlem  24300  xpsdsval  24302  xpsmet  24303  onint1  36430  pw2f1ocnv  43019  wepwsolem  43024  omnord1ex  43286  oege2  43289  df3o2  43295  oenord1ex  43297  oenord1  43298  oaomoencom  43299  oenassex  43300  omabs2  43314  omcl3g  43316  clsk1independent  44028  setc1onsubc  49584