Theorem res0 5973

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 5664	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5751	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4172	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4352	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2792	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1563  Vcvv 3457   ∩ cin 3906  ∅c0 4288   × cxp 5650   ↾ cres 5654

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-in 3914  df-nul 4289  df-opab 5168  df-xp 5658  df-res 5664

This theorem is referenced by:  ima0  6070  resdisj  6159  dfpo2  6287  smo0  8333  tfrlem16  8368  tz7.44-1  8381  rdg0n  8409  mapunen  9122  fnfi  9150  ackbij2lem3  10211  hashf1lem1  14482  setsid  17257  join0  18449  meet0  18450  frmdplusg  18903  psgn0fv0  19572  gsum2dlem2  20032  ablfac1eulem  20135  ablfac1eu  20136  gsumle  20206  psrplusg  22047  ply1plusgfvi  22361  ptuncnv  23925  ptcmpfi  23931  ust0  24338  xrge0gsumle  24952  xrge0tsms  24953  jensen  27111  egrsubgr  29536  0grsubgr  29537  pthdlem1  30024  0pth  30385  1pthdlem1  30395  eupth2lemb  30497  fressupp  32945  resf1o  32987  xrge0tsmsd  33306  rprmdvdsprod  33741  zarcmplem  34188  esumsnf  34371  satfv1lem  35725  eldm3  36124  rdgprc0  36154  bj-rdg0gALT  37568  zrdivrng  38464  disjresin  38754  eldioph4b  43400  diophren  43402  ismeannd  47039  psmeasure  47043  isomennd  47103  hoidmvlelem3  47169  stgr0  48580  tposres3  49510  setc1oid  50124  aacllem  50430