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

Theorem res0 5850
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 5560 . 2 (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2 0xp 5642 . . 3 (∅ × V) = ∅
32ineq2i 4183 . 2 (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4 in0 4342 . 2 (𝐴 ∩ ∅) = ∅
51, 3, 43eqtri 2845 1 (𝐴 ↾ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1528  Vcvv 3492  cin 3932  c0 4288   × cxp 5546  cres 5550
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790  ax-sep 5194  ax-nul 5201  ax-pr 5320
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-rab 3144  df-v 3494  df-dif 3936  df-un 3938  df-in 3940  df-ss 3949  df-nul 4289  df-if 4464  df-sn 4558  df-pr 4560  df-op 4564  df-opab 5120  df-xp 5554  df-res 5560
This theorem is referenced by:  ima0  5938  resdisj  6019  smo0  7984  tfrlem16  8018  tz7.44-1  8031  mapunen  8674  fnfi  8784  ackbij2lem3  9651  hashf1lem1  13801  setsid  16526  meet0  17735  join0  17736  frmdplusg  18007  psgn0fv0  18568  gsum2dlem2  19020  ablfac1eulem  19123  ablfac1eu  19124  psrplusg  20089  ply1plusgfvi  20338  ptuncnv  22343  ptcmpfi  22349  ust0  22755  xrge0gsumle  23368  xrge0tsms  23369  jensen  25493  egrsubgr  26986  0grsubgr  26987  pthdlem1  27474  0pth  27831  1pthdlem1  27841  eupth2lemb  27943  resf1o  30392  xrge0tsmsd  30619  gsumle  30652  esumsnf  31222  satfv1lem  32506  dfpo2  32888  eldm3  32894  rdgprc0  32935  zrdivrng  35112  eldioph4b  39286  diophren  39288  ismeannd  42626  psmeasure  42630  isomennd  42690  hoidmvlelem3  42756  aacllem  44830
  Copyright terms: Public domain W3C validator