Theorem df2o3 8513

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 8506	. 2 ⊢ 2o = suc 1o
2		df-suc 6392	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8512	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4174	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4634	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2766	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2767	1 ⊢ 2o = {∅, 1o}

Syntax hints:   = wceq 1537   ∪ cun 3961  ∅c0 4339  {csn 4631  {cpr 4633  suc csuc 6388  1_oc1o 8498  2_oc2o 8499

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-v 3480  df-dif 3966  df-un 3968  df-nul 4340  df-pr 4634  df-suc 6392  df-1o 8505  df-2o 8506

This theorem is referenced by:  df2o2  8514  2oex  8516  nlim2  8527  ord2eln012  8534  2oconcl  8540  enpr2d  9088  map2xp  9186  snnen2o  9271  rex2dom  9280  1sdom2dom  9281  1sdomOLD  9283  cantnflem2  9728  xp2dju  10215  sdom2en01  10340  sadcf  16487  fnpr2o  17604  fnpr2ob  17605  fvprif  17608  xpsfrnel  17609  xpsfeq  17610  xpsle  17626  setcepi  18142  setc2obas  18148  setc2ohom  18149  efgi0  19753  efgi1  19754  vrgpf  19801  vrgpinv  19802  frgpuptinv  19804  frgpup2  19809  frgpup3lem  19810  frgpnabllem1  19906  dmdprdpr  20084  dprdpr  20085  xpstopnlem1  23833  xpstopnlem2  23835  xpsxmetlem  24405  xpsdsval  24407  xpsmet  24408  onint1  36432  pw2f1ocnv  43026  wepwsolem  43031  omnord1ex  43294  oege2  43297  df3o2  43303  oenord1ex  43305  oenord1  43306  oaomoencom  43307  oenassex  43308  omabs2  43322  omcl3g  43324  clsk1independent  44036