Theorem res0 5948

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 5643	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5730	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4157	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4335	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2763	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1542  Vcvv 3429   ∩ cin 3888  ∅c0 4273   × cxp 5629   ↾ cres 5633

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-in 3896  df-nul 4274  df-opab 5148  df-xp 5637  df-res 5643

This theorem is referenced by:  ima0  6042  resdisj  6133  dfpo2  6260  smo0  8298  tfrlem16  8332  tz7.44-1  8345  rdg0n  8373  mapunen  9084  fnfi  9112  ackbij2lem3  10162  hashf1lem1  14417  setsid  17177  join0  18369  meet0  18370  frmdplusg  18822  psgn0fv0  19486  gsum2dlem2  19946  ablfac1eulem  20049  ablfac1eu  20050  gsumle  20120  psrplusg  21916  ply1plusgfvi  22205  ptuncnv  23772  ptcmpfi  23778  ust0  24185  xrge0gsumle  24799  xrge0tsms  24800  jensen  26952  egrsubgr  29346  0grsubgr  29347  pthdlem1  29834  0pth  30195  1pthdlem1  30205  eupth2lemb  30307  fressupp  32761  resf1o  32803  xrge0tsmsd  33134  rprmdvdsprod  33594  zarcmplem  34025  esumsnf  34208  satfv1lem  35544  eldm3  35943  rdgprc0  35973  bj-rdg0gALT  37378  zrdivrng  38274  disjresin  38564  eldioph4b  43239  diophren  43241  ismeannd  46895  psmeasure  46899  isomennd  46959  hoidmvlelem3  47025  stgr0  48436  tposres3  49356  setc1oid  49970  aacllem  50276