Theorem res0 5984

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 5675	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5762	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4171	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4353	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2790	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1570  Vcvv 3455   ∩ cin 3905  ∅c0 4287   × cxp 5661   ↾ cres 5665

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-in 3913  df-nul 4288  df-opab 5175  df-xp 5669  df-res 5675

This theorem is referenced by:  ima0  6081  resdisj  6169  dfpo2  6299  smo0  8346  tfrlem16  8381  tz7.44-1  8394  rdg0n  8422  mapunen  9135  fnfi  9163  ackbij2lem3  10224  hashf1lem1  14494  setsid  17268  join0  18460  meet0  18461  frmdplusg  18914  psgn0fv0  19582  gsum2dlem2  20042  ablfac1eulem  20145  ablfac1eu  20146  gsumle  20216  psrplusg  22068  ply1plusgfvi  22382  ptuncnv  23945  ptcmpfi  23951  ust0  24358  xrge0gsumle  24972  xrge0tsms  24973  jensen  27131  egrsubgr  29605  0grsubgr  29606  pthdlem1  30093  0pth  30454  1pthdlem1  30464  eupth2lemb  30566  fressupp  33011  resf1o  33053  xrge0tsmsd  33371  rprmdvdsprod  33802  zarcmplem  34249  esumsnf  34432  satfv1lem  35832  eldm3  36231  rdgprc0  36261  bj-rdg0gALT  37685  zrdivrng  38582  disjresin  38870  eldioph4b  43518  diophren  43520  ismeannd  47161  psmeasure  47165  isomennd  47225  hoidmvlelem3  47291  stgr0  48702  tposres3  49636  setc1oid  50250  aacllem  50578