Theorem res0 5970

Description: A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)

Assertion

Ref	Expression
res0	⊢ (𝐴 ↾ ∅) = ∅

Proof of Theorem res0

Step	Hyp	Ref	Expression
1		df-res 5666	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5753	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4192	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4370	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2762	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1540  Vcvv 3459   ∩ cin 3925  ∅c0 4308   × cxp 5652   ↾ cres 5656

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pr 5402

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-opab 5182  df-xp 5660  df-res 5666

This theorem is referenced by:  ima0  6064  resdisj  6158  dfpo2  6285  smo0  8372  tfrlem16  8407  tz7.44-1  8420  rdg0n  8448  mapunen  9160  fnfi  9192  ackbij2lem3  10254  hashf1lem1  14473  setsid  17226  join0  18415  meet0  18416  frmdplusg  18832  psgn0fv0  19492  gsum2dlem2  19952  ablfac1eulem  20055  ablfac1eu  20056  psrplusg  21896  ply1plusgfvi  22177  ptuncnv  23745  ptcmpfi  23751  ust0  24158  xrge0gsumle  24773  xrge0tsms  24774  jensen  26951  egrsubgr  29256  0grsubgr  29257  pthdlem1  29748  0pth  30106  1pthdlem1  30116  eupth2lemb  30218  fressupp  32665  resf1o  32707  xrge0tsmsd  33056  gsumle  33092  rprmdvdsprod  33549  zarcmplem  33912  esumsnf  34095  satfv1lem  35384  eldm3  35778  rdgprc0  35811  bj-rdg0gALT  37089  zrdivrng  37977  disjresin  38258  eldioph4b  42834  diophren  42836  ismeannd  46496  psmeasure  46500  isomennd  46560  hoidmvlelem3  46626  stgr0  47972  tposres3  48856  setc1oid  49380  aacllem  49665