Theorem df2o3 8496

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 8489	. 2 ⊢ 2o = suc 1o
2		df-suc 6369	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8495	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4144	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4609	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2760	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2761	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1539   ∪ cun 3929  ∅c0 4313  {csn 4606  {cpr 4608  suc csuc 6365  1_oc1o 8481  2_oc2o 8482

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3465  df-dif 3934  df-un 3936  df-nul 4314  df-pr 4609  df-suc 6369  df-1o 8488  df-2o 8489

This theorem is referenced by:  df2o2  8497  2oex  8499  nlim2  8510  ord2eln012  8517  2oconcl  8523  enpr2d  9071  map2xp  9169  snnen2o  9255  rex2dom  9264  1sdom2dom  9265  1sdomOLD  9267  cantnflem2  9712  xp2dju  10199  sdom2en01  10324  sadcf  16473  fnpr2o  17574  fnpr2ob  17575  fvprif  17578  xpsfrnel  17579  xpsfeq  17580  xpsle  17596  setcepi  18105  setc2obas  18111  setc2ohom  18112  efgi0  19707  efgi1  19708  vrgpf  19755  vrgpinv  19756  frgpuptinv  19758  frgpup2  19763  frgpup3lem  19764  frgpnabllem1  19860  dmdprdpr  20038  dprdpr  20039  xpstopnlem1  23764  xpstopnlem2  23766  xpsxmetlem  24335  xpsdsval  24337  xpsmet  24338  onint1  36425  pw2f1ocnv  43027  wepwsolem  43032  omnord1ex  43294  oege2  43297  df3o2  43303  oenord1ex  43305  oenord1  43306  oaomoencom  43307  oenassex  43308  omabs2  43322  omcl3g  43324  clsk1independent  44036