Theorem res0 5884

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 5592	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5675	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4140	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4322	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2770	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1539  Vcvv 3422   ∩ cin 3882  ∅c0 4253   × cxp 5578   ↾ cres 5582

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709  ax-sep 5218  ax-nul 5225  ax-pr 5347

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-opab 5133  df-xp 5586  df-res 5592

This theorem is referenced by:  ima0  5974  resdisj  6061  dfpo2  6188  smo0  8160  tfrlem16  8195  tz7.44-1  8208  mapunen  8882  fnfi  8925  ackbij2lem3  9928  hashf1lem1  14096  hashf1lem1OLD  14097  setsid  16837  join0  18038  meet0  18039  frmdplusg  18408  psgn0fv0  19034  gsum2dlem2  19487  ablfac1eulem  19590  ablfac1eu  19591  psrplusg  21060  ply1plusgfvi  21323  ptuncnv  22866  ptcmpfi  22872  ust0  23279  xrge0gsumle  23902  xrge0tsms  23903  jensen  26043  egrsubgr  27547  0grsubgr  27548  pthdlem1  28035  0pth  28390  1pthdlem1  28400  eupth2lemb  28502  fressupp  30924  resf1o  30967  xrge0tsmsd  31219  gsumle  31252  zarcmplem  31733  esumsnf  31932  satfv1lem  33224  rdg0n  33598  eldm3  33634  rdgprc0  33675  bj-rdg0gALT  35169  zrdivrng  36038  eldioph4b  40549  diophren  40551  ismeannd  43895  psmeasure  43899  isomennd  43959  hoidmvlelem3  44025  aacllem  46391