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 5637	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5724	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4153	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4330	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2767	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1547  Vcvv 3432   ∩ cin 3889  ∅c0 4268   × cxp 5623   ↾ cres 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-in 3897  df-nul 4269  df-opab 5142  df-xp 5631  df-res 5637

This theorem is referenced by:  ima0  6036  resdisj  6127  dfpo2  6254  smo0  8295  tfrlem16  8329  tz7.44-1  8342  rdg0n  8370  mapunen  9081  fnfi  9109  ackbij2lem3  10160  hashf1lem1  14415  setsid  17175  join0  18367  meet0  18368  frmdplusg  18820  psgn0fv0  19484  gsum2dlem2  19944  ablfac1eulem  20047  ablfac1eu  20048  gsumle  20118  psrplusg  21919  ply1plusgfvi  22233  ptuncnv  23797  ptcmpfi  23803  ust0  24210  xrge0gsumle  24824  xrge0tsms  24825  jensen  26977  egrsubgr  29371  0grsubgr  29372  pthdlem1  29859  0pth  30220  1pthdlem1  30230  eupth2lemb  30332  fressupp  32787  resf1o  32829  xrge0tsmsd  33161  rprmdvdsprod  33624  zarcmplem  34072  esumsnf  34255  satfv1lem  35597  eldm3  35996  rdgprc0  36026  bj-rdg0gALT  37431  zrdivrng  38327  disjresin  38617  eldioph4b  43263  diophren  43265  ismeannd  46917  psmeasure  46921  isomennd  46981  hoidmvlelem3  47047  stgr0  48458  tposres3  49378  setc1oid  49992  aacllem  50298