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

Theorem res0 5553
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 5276 . 2 (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2 0xp 5354 . . 3 (∅ × V) = ∅
32ineq2i 3952 . 2 (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4 in0 4109 . 2 (𝐴 ∩ ∅) = ∅
51, 3, 43eqtri 2784 1 (𝐴 ↾ ∅) = ∅
Colors of variables: wff setvar class
Syntax hints:   = wceq 1630  Vcvv 3338  cin 3712  c0 4056   × cxp 5262  cres 5266
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1986  ax-6 2052  ax-7 2088  ax-9 2146  ax-10 2166  ax-11 2181  ax-12 2194  ax-13 2389  ax-ext 2738  ax-sep 4931  ax-nul 4939  ax-pr 5053
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2045  df-clab 2745  df-cleq 2751  df-clel 2754  df-nfc 2889  df-v 3340  df-dif 3716  df-un 3718  df-in 3720  df-ss 3727  df-nul 4057  df-if 4229  df-sn 4320  df-pr 4322  df-op 4326  df-opab 4863  df-xp 5270  df-res 5276
This theorem is referenced by:  ima0  5637  resdisj  5719  smo0  7622  tfrlem16  7656  tz7.44-1  7669  mapunen  8292  fnfi  8401  ackbij2lem3  9253  hashf1lem1  13429  setsid  16114  meet0  17336  join0  17337  frmdplusg  17590  psgn0fv0  18129  gsum2dlem2  18568  ablfac1eulem  18669  ablfac1eu  18670  psrplusg  19581  ply1plusgfvi  19812  ptuncnv  21810  ptcmpfi  21816  ust0  22222  xrge0gsumle  22835  xrge0tsms  22836  jensen  24912  egrsubgr  26366  0grsubgr  26367  pthdlem1  26870  0pth  27275  1pthdlem1  27285  eupth2lemb  27387  resf1o  29812  gsumle  30086  xrge0tsmsd  30092  esumsnf  30433  dfpo2  31950  eldm3  31956  rdgprc0  32002  zrdivrng  34063  eldioph4b  37875  diophren  37877  ismeannd  41185  psmeasure  41189  isomennd  41249  hoidmvlelem3  41315  aacllem  43058
  Copyright terms: Public domain W3C validator