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

Theorem res0 5307
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 5039 . 2 (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2 0xp 5111 . . 3 (∅ × V) = ∅
32ineq2i 3772 . 2 (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4 in0 3919 . 2 (𝐴 ∩ ∅) = ∅
51, 3, 43eqtri 2635 1 (𝐴 ↾ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1474  Vcvv 3172  cin 3538  c0 3873   × cxp 5025  cres 5029
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-9 1985  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589  ax-sep 4703  ax-nul 4711  ax-pr 4827
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-opab 4638  df-xp 5033  df-res 5039
This theorem is referenced by:  ima0  5386  resdisj  5467  smo0  7319  tfrlem16  7353  tz7.44-1  7366  mapunen  7991  fnfi  8100  ackbij2lem3  8923  hashf1lem1  13050  setsid  15690  meet0  16908  join0  16909  frmdplusg  17162  psgn0fv0  17702  gsum2dlem2  18141  ablfac1eulem  18242  ablfac1eu  18243  psrplusg  19150  ply1plusgfvi  19381  ptuncnv  21367  ptcmpfi  21373  ust0  21780  xrge0gsumle  22391  xrge0tsms  22392  jensen  24459  0pth  25893  1pthonlem1  25912  eupath2  26300  resf1o  28686  gsumle  28903  xrge0tsmsd  28909  esumsnf  29246  dfpo2  30691  eldm3  30698  rdgprc0  30736  zrdivrng  32705  eldioph4b  36176  diophren  36178  ismeannd  39143  psmeasure  39147  isomennd  39204  hoidmvlelem3  39270  egrsubgr  40482  0grsubgr  40483  pthdlem1  40953  0pth-av  41274  1pthdlem1  41283  eupth2lemb  41386  aacllem  42298
  Copyright terms: Public domain W3C validator