MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df2o3 Structured version   Visualization version   GIF version

Theorem df2o3 8421
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
StepHypRef Expression
1 df-2o 8414 . 2 2o = suc 1o
2 df-suc 6324 . 2 suc 1o = (1o ∪ {1o})
3 df1o2 8420 . . . 4 1o = {∅}
43uneq1i 4120 . . 3 (1o ∪ {1o}) = ({∅} ∪ {1o})
5 df-pr 4590 . . 3 {∅, 1o} = ({∅} ∪ {1o})
64, 5eqtr4i 2768 . 2 (1o ∪ {1o}) = {∅, 1o}
71, 2, 63eqtri 2769 1 2o = {∅, 1o}
Colors of variables: wff setvar class
Syntax hints:   = wceq 1542  cun 3909  c0 4283  {csn 4587  {cpr 4589  suc csuc 6320  1oc1o 8406  2oc2o 8407
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3448  df-dif 3914  df-un 3916  df-nul 4284  df-pr 4590  df-suc 6324  df-1o 8413  df-2o 8414
This theorem is referenced by:  df2o2  8422  2oex  8424  nlim2  8437  ord2eln012  8444  2oconcl  8450  enpr2d  8994  map2xp  9092  snnen2o  9182  rex2dom  9191  1sdom2dom  9192  1sdomOLD  9194  cantnflem2  9627  xp2dju  10113  sdom2en01  10239  sadcf  16334  fnpr2o  17440  fnpr2ob  17441  fvprif  17444  xpsfrnel  17445  xpsfeq  17446  xpsle  17462  setcepi  17975  setc2obas  17981  setc2ohom  17982  efgi0  19503  efgi1  19504  vrgpf  19551  vrgpinv  19552  frgpuptinv  19554  frgpup2  19559  frgpup3lem  19560  frgpnabllem1  19652  dmdprdpr  19829  dprdpr  19830  xpstopnlem1  23163  xpstopnlem2  23165  xpsxmetlem  23735  xpsdsval  23737  xpsmet  23738  onint1  34924  pw2f1ocnv  41364  wepwsolem  41372  omnord1ex  41641  oege2  41644  df3o2  41650  oenord1ex  41652  oenord1  41653  oaomoencom  41654  oenassex  41655  omabs2  41668  omcl3g  41670  clsk1independent  42325
  Copyright terms: Public domain W3C validator