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

Theorem res0 5090
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 4830 . 2  |-  ( A  |`  (/) )  =  ( A  i^i  ( (/)  X. 
_V ) )
2 xp0r 4896 . . 3  |-  ( (/)  X. 
_V )  =  (/)
32ineq2i 3482 . 2  |-  ( A  i^i  ( (/)  X.  _V ) )  =  ( A  i^i  (/) )
4 in0 3596 . 2  |-  ( A  i^i  (/) )  =  (/)
51, 3, 43eqtri 2411 1  |-  ( A  |`  (/) )  =  (/)
Colors of variables: wff set class
Syntax hints:    = wceq 1649   _Vcvv 2899    i^i cin 3262   (/)c0 3571    X. cxp 4816    |` cres 4820
This theorem is referenced by:  ima0  5161  resdisj  5238  smo0  6556  tfrlem16  6590  tz7.44-1  6600  mapunen  7212  fnfi  7320  ackbij2lem3  8054  hashf1lem1  11631  setsid  13435  frmdplusg  14726  gsum2d  15473  ablfac1eulem  15557  ablfac1eu  15558  psrplusg  16372  ply1plusgfvi  16563  ptuncnv  17760  ptcmpfi  17766  ust0  18170  xrge0gsumle  18735  xrge0tsms  18736  jensen  20694  0pth  21424  1pthonlem1  21437  eupath2  21550  zrdivrng  21868  xrge0tsmsd  24052  esumsn  24252  dfpo2  25136  eldm3  25143  rdgprc0  25174  eldioph4b  26563  diophren  26565
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1661  ax-8 1682  ax-14 1721  ax-6 1736  ax-7 1741  ax-11 1753  ax-12 1939  ax-ext 2368  ax-sep 4271  ax-nul 4279  ax-pr 4344
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3an 938  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2374  df-cleq 2380  df-clel 2383  df-nfc 2512  df-ne 2552  df-v 2901  df-dif 3266  df-un 3268  df-in 3270  df-ss 3277  df-nul 3572  df-if 3683  df-sn 3763  df-pr 3764  df-op 3766  df-opab 4208  df-xp 4824  df-res 4830
  Copyright terms: Public domain W3C validator