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

Theorem res0 5127
Description: A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)
Assertion
Ref Expression
res0  |-  ( A  |`  (/) )  =  (/)

Proof of Theorem res0
StepHypRef Expression
1 df-res 4864 . 2  |-  ( A  |`  (/) )  =  ( A  i^i  ( (/)  X. 
_V ) )
2 0xp 4933 . . 3  |-  ( (/)  X. 
_V )  =  (/)
32ineq2i 3642 . 2  |-  ( A  i^i  ( (/)  X.  _V ) )  =  ( A  i^i  (/) )
4 in0 3771 . 2  |-  ( A  i^i  (/) )  =  (/)
51, 3, 43eqtri 2487 1  |-  ( A  |`  (/) )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1454   _Vcvv 3056    i^i cin 3414   (/)c0 3742    X. cxp 4850    |` cres 4854
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1679  ax-4 1692  ax-5 1768  ax-6 1815  ax-7 1861  ax-9 1906  ax-10 1925  ax-11 1930  ax-12 1943  ax-13 2101  ax-ext 2441  ax-sep 4538  ax-nul 4547  ax-pr 4652
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1457  df-ex 1674  df-nf 1678  df-sb 1808  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2591  df-ne 2634  df-v 3058  df-dif 3418  df-un 3420  df-in 3422  df-ss 3429  df-nul 3743  df-if 3893  df-sn 3980  df-pr 3982  df-op 3986  df-opab 4475  df-xp 4858  df-res 4864
This theorem is referenced by:  ima0  5201  resdisj  5284  smo0  7102  tfrlem16  7136  tz7.44-1  7149  mapunen  7766  fnfi  7874  ackbij2lem3  8696  hashf1lem1  12650  setsid  15212  meet0  16431  join0  16432  frmdplusg  16686  psgn0fv0  17200  gsum2dlem2  17651  ablfac1eulem  17753  ablfac1eu  17754  psrplusg  18653  ply1plusgfvi  18883  ptuncnv  20870  ptcmpfi  20876  ust0  21282  xrge0gsumle  21899  xrge0tsms  21900  jensen  23962  0pth  25348  1pthonlem1  25367  eupath2  25756  zrdivrng  26208  resf1o  28363  gsumle  28590  xrge0tsmsd  28596  esumsnf  28933  dfpo2  30443  eldm3  30450  rdgprc0  30488  eldioph4b  35698  diophren  35700  ismeannd  38342  psmeasure  38346  isomennd  38389  hoidmvlelem3  38456  egrsubgr  39398  0grsubgr  39399  pthdlem1  39791  0pth-av  39840  1pthdlem1  39849  aacllem  40812
  Copyright terms: Public domain W3C validator