Theorem df2o3 8396

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 8389	. 2 ⊢ 2o = suc 1o
2		df-suc 6313	. 2 ⊢ suc 1o = (1o ∪ {1o})
3		df1o2 8395	. . . 4 ⊢ 1o = {∅}
4	3	uneq1i 4115	. . 3 ⊢ (1o ∪ {1o}) = ({∅} ∪ {1o})
5		df-pr 4580	. . 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 3901  ∅c0 4284  {csn 4577  {cpr 4579  suc csuc 6309  1_oc1o 8381  2_oc2o 8382

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 3438  df-dif 3906  df-un 3908  df-nul 4285  df-pr 4580  df-suc 6313  df-1o 8388  df-2o 8389

This theorem is referenced by:  df2o2  8397  2oex  8399  nlim2  8408  ord2eln012  8415  2oconcl  8421  enpr2d  8974  map2xp  9064  snnen2o  9134  rex2dom  9142  1sdom2dom  9143  cantnflem2  9586  xp2dju  10071  sdom2en01  10196  sadcf  16364  fnpr2o  17461  fnpr2ob  17462  fvprif  17465  xpsfrnel  17466  xpsfeq  17467  xpsle  17483  setcepi  17995  setc2obas  18001  setc2ohom  18002  efgi0  19599  efgi1  19600  vrgpf  19647  vrgpinv  19648  frgpuptinv  19650  frgpup2  19655  frgpup3lem  19656  frgpnabllem1  19752  dmdprdpr  19930  dprdpr  19931  xpstopnlem1  23694  xpstopnlem2  23696  xpsxmetlem  24265  xpsdsval  24267  xpsmet  24268  onint1  36427  pw2f1ocnv  43014  wepwsolem  43019  omnord1ex  43281  oege2  43284  df3o2  43290  oenord1ex  43292  oenord1  43293  oaomoencom  43294  oenassex  43295  omabs2  43309  omcl3g  43311  clsk1independent  44023  setc1onsubc  49591