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

Theorem res0 4959
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 4701 . 2  |-  ( A  |`  (/) )  =  ( A  i^i  ( (/)  X. 
_V ) )
2 xp0r 4768 . . 3  |-  ( (/)  X. 
_V )  =  (/)
32ineq2i 3367 . 2  |-  ( A  i^i  ( (/)  X.  _V ) )  =  ( A  i^i  (/) )
4 in0 3480 . 2  |-  ( A  i^i  (/) )  =  (/)
51, 3, 43eqtri 2307 1  |-  ( A  |`  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1623   _Vcvv 2788    i^i cin 3151   (/)c0 3455    X. cxp 4687    |` cres 4691
This theorem is referenced by:  ima0  5030  resdisj  5105  smo0  6375  tfrlem16  6409  tz7.44-1  6419  mapunen  7030  fnfi  7134  ackbij2lem3  7867  hashf1lem1  11393  setsid  13187  frmdplusg  14476  gsum2d  15223  ablfac1eulem  15307  ablfac1eu  15308  psrplusg  16126  ply1plusgfvi  16320  ptuncnv  17498  ptcmpfi  17504  xrge0gsumle  18338  xrge0tsms  18339  jensen  20283  zrdivrng  21099  xrge0tsmsd  23382  esumsn  23437  eupath2  23904  dfpo2  24112  eldm3  24119  rdgprc0  24150  empos  25242  eldioph4b  26894  diophren  26896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-sep 4141  ax-nul 4149  ax-pr 4214
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-v 2790  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-sn 3646  df-pr 3647  df-op 3649  df-opab 4078  df-xp 4695  df-res 4701
  Copyright terms: Public domain W3C validator