Theorem res0 5942

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 5636	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5723	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4158	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4336	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2764	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1542  Vcvv 3430   ∩ cin 3889  ∅c0 4274   × cxp 5622   ↾ cres 5626

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 3391  df-v 3432  df-dif 3893  df-in 3897  df-nul 4275  df-opab 5149  df-xp 5630  df-res 5636

This theorem is referenced by:  ima0  6036  resdisj  6127  dfpo2  6254  smo0  8291  tfrlem16  8325  tz7.44-1  8338  rdg0n  8366  mapunen  9077  fnfi  9105  ackbij2lem3  10153  hashf1lem1  14408  setsid  17168  join0  18360  meet0  18361  frmdplusg  18813  psgn0fv0  19477  gsum2dlem2  19937  ablfac1eulem  20040  ablfac1eu  20041  gsumle  20111  psrplusg  21926  ply1plusgfvi  22215  ptuncnv  23782  ptcmpfi  23788  ust0  24195  xrge0gsumle  24809  xrge0tsms  24810  jensen  26966  egrsubgr  29360  0grsubgr  29361  pthdlem1  29849  0pth  30210  1pthdlem1  30220  eupth2lemb  30322  fressupp  32776  resf1o  32818  xrge0tsmsd  33149  rprmdvdsprod  33609  zarcmplem  34041  esumsnf  34224  satfv1lem  35560  eldm3  35959  rdgprc0  35989  bj-rdg0gALT  37394  zrdivrng  38288  disjresin  38578  eldioph4b  43257  diophren  43259  ismeannd  46913  psmeasure  46917  isomennd  46977  hoidmvlelem3  47043  stgr0  48448  tposres3  49368  setc1oid  49982  aacllem  50288