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

Theorem df2o3 6576
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 6564 . 2  |-  2o  =  suc  1o
2 df-suc 4477 . 2  |-  suc  1o  =  ( 1o  u.  { 1o } )
3 df1o2 6575 . . . 4  |-  1o  =  { (/) }
43uneq1i 3401 . . 3  |-  ( 1o  u.  { 1o }
)  =  ( {
(/) }  u.  { 1o } )
5 df-pr 3723 . . 3  |-  { (/) ,  1o }  =  ( { (/) }  u.  { 1o } )
64, 5eqtr4i 2381 . 2  |-  ( 1o  u.  { 1o }
)  =  { (/) ,  1o }
71, 2, 63eqtri 2382 1  |-  2o  =  { (/) ,  1o }
Colors of variables: wff set class
Syntax hints:    = wceq 1642    u. cun 3226   (/)c0 3531   {csn 3716   {cpr 3717   suc csuc 4473   1oc1o 6556   2oc2o 6557
This theorem is referenced by:  df2o2  6577  2oconcl  6586  map2xp  7116  1sdom  7150  cantnflem2  7479  xp2cda  7893  sdom2en01  8015  sadcf  12735  xpscfn  13554  xpscfv  13557  xpsfrnel  13558  xpsfeq  13559  xpsfrnel2  13560  xpsle  13576  setcepi  14013  efgi0  15122  efgi1  15123  vrgpf  15170  vrgpinv  15171  frgpuptinv  15173  frgpup2  15178  frgpup3lem  15179  frgpnabllem1  15254  dmdprdpr  15377  dprdpr  15378  xpstopnlem1  17600  xpstopnlem2  17602  xpsxmetlem  18039  xpsdsval  18041  xpsmet  18042  onint1  25447  pw2f1ocnv  26453  wepwsolem  26461
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-v 2866  df-dif 3231  df-un 3233  df-nul 3532  df-pr 3723  df-suc 4477  df-1o 6563  df-2o 6564
  Copyright terms: Public domain W3C validator