Theorem df2o3 8484

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 8477	. 2 ⊢ 2o = suc 1o
2		df-suc 6368	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8483	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4111	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4587	. . 3 ⊢ {∅, 1o} = ({∅} ∪ {1o})
6	4, 5	eqtr4i 2787	. 2 ⊢ (1o ∪ {1o}) = {∅, 1o}
7	1, 2, 6	3eqtri 2788	1 ⊢ 2o = {∅, 1o}

This proof depends on syntax axioms:   = wceq 1570   ∪ cun 3897  ∅c0 4279  {csn 4584  {cpr 4586  suc csuc 6364  1_oc1o 8469  2_oc2o 8470

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-dif 3902  df-un 3904  df-nul 4280  df-pr 4587  df-suc 6368  df-1o 8476  df-2o 8477

This theorem is used by:  df2o2  8485  2oex  8488  nlim2  8498  ord2eln012  8505  2oconcl  8511  enpr2d  9076  map2xp  9166  snnen2o  9236  rex2dom  9244  1sdom2dom  9245  cantnflem2  9691  xp2dju  10255  sdom2en01  10380  sadcf  16623  fnpr2o  17729  fnpr2ob  17730  fvprif  17733  xpsfrnel  17734  xpsfeq  17735  xpsle  17751  setcepi  18263  setc2obas  18269  setc2ohom  18270  efgi0  19934  efgi1  19935  vrgpf  19982  vrgpinv  19983  frgpuptinv  19985  frgpup2  19990  frgpup3lem  19991  frgpnabllem1  20087  dmdprdpr  20265  dprdpr  20266  xpstopnlem1  24128  xpstopnlem2  24130  xpsxmetlem  24698  xpsdsval  24700  xpsmet  24701  bdaypw2n0bndlem  28849  onint1  37237  pw2f1ocnv  44043  wepwsolem  44048  omnord1ex  44305  oege2  44308  df3o2  44314  oenord1ex  44316  oenord1  44317  oaomoencom  44318  oenassex  44319  omabs2  44333  omcl3g  44335  clsk1independent  45045  setc1onsubc  50709