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

Theorem res0 5226
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 4963 . 2  |-  ( A  |`  (/) )  =  ( A  i^i  ( (/)  X. 
_V ) )
2 0xp 5028 . . 3  |-  ( (/)  X. 
_V )  =  (/)
32ineq2i 3660 . 2  |-  ( A  i^i  ( (/)  X.  _V ) )  =  ( A  i^i  (/) )
4 in0 3774 . 2  |-  ( A  i^i  (/) )  =  (/)
51, 3, 43eqtri 2487 1  |-  ( A  |`  (/) )  =  (/)
Colors of variables: wff setvar class
Syntax hints:    = wceq 1370   _Vcvv 3078    i^i cin 3438   (/)c0 3748    X. cxp 4949    |` cres 4953
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-opab 4462  df-xp 4957  df-res 4963
This theorem is referenced by:  ima0  5295  resdisj  5378  smo0  6932  tfrlem16  6965  tz7.44-1  6975  mapunen  7593  fnfi  7703  ackbij2lem3  8524  hashf1lem1  12329  setsid  14336  meet0  15429  join0  15430  frmdplusg  15654  psgn0fv0  16139  gsum2dlem2  16587  gsum2dOLD  16589  ablfac1eulem  16698  ablfac1eu  16699  psrplusg  17578  ply1plusgfvi  17823  ptuncnv  19515  ptcmpfi  19521  ust0  19929  xrge0gsumle  20545  xrge0tsms  20546  jensen  22518  0pth  23641  1pthonlem1  23660  eupath2  23773  zrdivrng  24091  resf1o  26201  gsumle  26411  xrge0tsmsd  26418  esumsn  26680  dfpo2  27729  eldm3  27736  rdgprc0  27771  eldioph4b  29318  diophren  29320
  Copyright terms: Public domain W3C validator