Theorem res0 5936

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 5631	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5718	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4166	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4344	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2760	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1541  Vcvv 3437   ∩ cin 3897  ∅c0 4282   × cxp 5617   ↾ cres 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-in 3905  df-nul 4283  df-opab 5156  df-xp 5625  df-res 5631

This theorem is referenced by:  ima0  6030  resdisj  6121  dfpo2  6248  smo0  8284  tfrlem16  8318  tz7.44-1  8331  rdg0n  8359  mapunen  9066  fnfi  9094  ackbij2lem3  10138  hashf1lem1  14364  setsid  17120  join0  18311  meet0  18312  frmdplusg  18764  psgn0fv0  19425  gsum2dlem2  19885  ablfac1eulem  19988  ablfac1eu  19989  gsumle  20059  psrplusg  21875  ply1plusgfvi  22155  ptuncnv  23723  ptcmpfi  23729  ust0  24136  xrge0gsumle  24750  xrge0tsms  24751  jensen  26927  egrsubgr  29257  0grsubgr  29258  pthdlem1  29746  0pth  30107  1pthdlem1  30117  eupth2lemb  30219  fressupp  32673  resf1o  32717  xrge0tsmsd  33049  rprmdvdsprod  33506  zarcmplem  33915  esumsnf  34098  satfv1lem  35427  eldm3  35826  rdgprc0  35856  bj-rdg0gALT  37136  zrdivrng  38014  disjresin  38299  eldioph4b  42929  diophren  42931  ismeannd  46590  psmeasure  46594  isomennd  46654  hoidmvlelem3  46720  stgr0  48085  tposres3  49006  setc1oid  49621  aacllem  49927