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

Theorem res0 5605
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 5325 . 2 (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2 0xp 5405 . . 3 (∅ × V) = ∅
32ineq2i 4010 . 2 (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4 in0 4165 . 2 (𝐴 ∩ ∅) = ∅
51, 3, 43eqtri 2826 1 (𝐴 ↾ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1653  Vcvv 3386  cin 3769  c0 4116   × cxp 5311  cres 5315
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-sep 4976  ax-nul 4984  ax-pr 5098
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-opab 4907  df-xp 5319  df-res 5325
This theorem is referenced by:  ima0  5699  resdisj  5781  smo0  7695  tfrlem16  7729  tz7.44-1  7742  mapunen  8372  fnfi  8481  ackbij2lem3  9352  hashf1lem1  13487  setsid  16238  meet0  17451  join0  17452  frmdplusg  17706  psgn0fv0  18243  gsum2dlem2  18684  ablfac1eulem  18786  ablfac1eu  18787  psrplusg  19703  ply1plusgfvi  19933  ptuncnv  21938  ptcmpfi  21944  ust0  22350  xrge0gsumle  22963  xrge0tsms  22964  jensen  25066  egrsubgr  26510  0grsubgr  26511  pthdlem1  27019  0pth  27468  1pthdlem1  27478  eupth2lemb  27581  resf1o  30022  gsumle  30294  xrge0tsmsd  30300  esumsnf  30641  dfpo2  32158  eldm3  32164  rdgprc0  32210  zrdivrng  34238  eldioph4b  38156  diophren  38158  ismeannd  41422  psmeasure  41426  isomennd  41486  hoidmvlelem3  41552  aacllem  43344
  Copyright terms: Public domain W3C validator