Theorem res0 5895

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 5601	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5685	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4143	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4325	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2770	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1539  Vcvv 3432   ∩ cin 3886  ∅c0 4256   × cxp 5587   ↾ cres 5591

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2709  ax-sep 5223  ax-nul 5230  ax-pr 5352

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1783  df-sb 2068  df-clab 2716  df-cleq 2730  df-clel 2816  df-rab 3073  df-v 3434  df-dif 3890  df-un 3892  df-in 3894  df-nul 4257  df-if 4460  df-sn 4562  df-pr 4564  df-op 4568  df-opab 5137  df-xp 5595  df-res 5601

This theorem is referenced by:  ima0  5985  resdisj  6072  dfpo2  6199  smo0  8189  tfrlem16  8224  tz7.44-1  8237  rdg0n  8265  mapunen  8933  fnfi  8964  ackbij2lem3  9997  hashf1lem1  14168  hashf1lem1OLD  14169  setsid  16909  join0  18123  meet0  18124  frmdplusg  18493  psgn0fv0  19119  gsum2dlem2  19572  ablfac1eulem  19675  ablfac1eu  19676  psrplusg  21150  ply1plusgfvi  21413  ptuncnv  22958  ptcmpfi  22964  ust0  23371  xrge0gsumle  23996  xrge0tsms  23997  jensen  26138  egrsubgr  27644  0grsubgr  27645  pthdlem1  28134  0pth  28489  1pthdlem1  28499  eupth2lemb  28601  fressupp  31022  resf1o  31065  xrge0tsmsd  31317  gsumle  31350  zarcmplem  31831  esumsnf  32032  satfv1lem  33324  eldm3  33728  rdgprc0  33769  bj-rdg0gALT  35242  zrdivrng  36111  eldioph4b  40633  diophren  40635  ismeannd  44005  psmeasure  44009  isomennd  44069  hoidmvlelem3  44135  aacllem  46505