Theorem res0 6001

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 5697	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5784	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4217	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4395	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2769	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1540  Vcvv 3480   ∩ cin 3950  ∅c0 4333   × cxp 5683   ↾ cres 5687

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 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-opab 5206  df-xp 5691  df-res 5697

This theorem is referenced by:  ima0  6095  resdisj  6189  dfpo2  6316  smo0  8398  tfrlem16  8433  tz7.44-1  8446  rdg0n  8474  mapunen  9186  fnfi  9218  ackbij2lem3  10280  hashf1lem1  14494  setsid  17244  join0  18450  meet0  18451  frmdplusg  18867  psgn0fv0  19529  gsum2dlem2  19989  ablfac1eulem  20092  ablfac1eu  20093  psrplusg  21956  ply1plusgfvi  22243  ptuncnv  23815  ptcmpfi  23821  ust0  24228  xrge0gsumle  24855  xrge0tsms  24856  jensen  27032  egrsubgr  29294  0grsubgr  29295  pthdlem1  29786  0pth  30144  1pthdlem1  30154  eupth2lemb  30256  fressupp  32697  resf1o  32741  xrge0tsmsd  33065  gsumle  33101  rprmdvdsprod  33562  zarcmplem  33880  esumsnf  34065  satfv1lem  35367  eldm3  35761  rdgprc0  35794  bj-rdg0gALT  37072  zrdivrng  37960  disjresin  38241  eldioph4b  42822  diophren  42824  ismeannd  46482  psmeasure  46486  isomennd  46546  hoidmvlelem3  46612  stgr0  47927  tposres3  48781  aacllem  49320