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

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

Proof of Theorem res0
StepHypRef Expression
1 df-res 5016 . 2
2 0xp 5085 . . 3
32ineq2i 3696 . 2
4 in0 3811 . 2
51, 3, 43eqtri 2490 1
Colors of variables: wff setvar class
Syntax hints:  =wceq 1395   cvv 3109  i^icin 3474   c0 3784  X.cxp 5002  |`cres 5006
This theorem is referenced by:  ima0  5357  resdisj  5441  smo0  7048  tfrlem16  7081  tz7.44-1  7091  mapunen  7706  fnfi  7818  ackbij2lem3  8642  hashf1lem1  12504  setsid  14673  meet0  15767  join0  15768  frmdplusg  16022  psgn0fv0  16536  gsum2dlem2  16998  gsum2dOLD  17000  ablfac1eulem  17123  ablfac1eu  17124  psrplusg  18034  ply1plusgfvi  18283  ptuncnv  20308  ptcmpfi  20314  ust0  20722  xrge0gsumle  21338  xrge0tsms  21339  jensen  23318  0pth  24572  1pthonlem1  24591  eupath2  24980  zrdivrng  25434  resf1o  27553  gsumle  27770  xrge0tsmsd  27775  esumsn  28072  dfpo2  29184  eldm3  29191  rdgprc0  29226  eldioph4b  30745  diophren  30747  aacllem  33216
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-opab 4511  df-xp 5010  df-res 5016
  Copyright terms: Public domain W3C validator