Theorem res0 5950

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 5644	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5731	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4171	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4349	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2764	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1542  Vcvv 3442   ∩ cin 3902  ∅c0 4287   × cxp 5630   ↾ cres 5634

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-in 3910  df-nul 4288  df-opab 5163  df-xp 5638  df-res 5644

This theorem is referenced by:  ima0  6044  resdisj  6135  dfpo2  6262  smo0  8300  tfrlem16  8334  tz7.44-1  8347  rdg0n  8375  mapunen  9086  fnfi  9114  ackbij2lem3  10162  hashf1lem1  14390  setsid  17146  join0  18338  meet0  18339  frmdplusg  18791  psgn0fv0  19452  gsum2dlem2  19912  ablfac1eulem  20015  ablfac1eu  20016  gsumle  20086  psrplusg  21904  ply1plusgfvi  22194  ptuncnv  23763  ptcmpfi  23769  ust0  24176  xrge0gsumle  24790  xrge0tsms  24791  jensen  26967  egrsubgr  29362  0grsubgr  29363  pthdlem1  29851  0pth  30212  1pthdlem1  30222  eupth2lemb  30324  fressupp  32777  resf1o  32819  xrge0tsmsd  33166  rprmdvdsprod  33626  zarcmplem  34058  esumsnf  34241  satfv1lem  35575  eldm3  35974  rdgprc0  36004  bj-rdg0gALT  37313  zrdivrng  38198  disjresin  38488  eldioph4b  43162  diophren  43164  ismeannd  46819  psmeasure  46823  isomennd  46883  hoidmvlelem3  46949  stgr0  48314  tposres3  49234  setc1oid  49848  aacllem  50154