Theorem res0 5985

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 5667	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5755	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4117	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4348	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2790	1 ⊢ (𝐴 ↾ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3454   ∩ cin 4092  ∅c0 4281   × cxp 5653   ↾ cres 5657

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-dif 4050  df-in 4094  df-nul 4282  df-opab 5171  df-xp 5661  df-res 5667

This theorem is used by:  ima0  6087  resdisj  6173  dfpo2  6317  smo0  8394  tfrlem16  8429  tz7.44-1  8442  rdg0n  8470  mapunen  9193  fnfi  9221  ackbij2lem3  10345  hashf1lem1  14627  setsid  17414  join0  18606  meet0  18607  frmdplusg  19079  psgn0fv0  19755  gsum2dlem2  20215  ablfac1eulem  20318  ablfac1eu  20319  gsumle  20389  psrplusg  22275  ply1plusgfvi  22589  ptuncnv  24156  ptcmpfi  24162  ust0  24569  xrge0gsumle  25183  xrge0tsms  25184  jensen  27346  egrsubgr  29888  0grsubgr  29889  pthdlem1  30382  0pth  30746  1pthdlem1  30756  eupth2lemb  30868  fressupp  33352  resf1o  33392  xrge0tsmsd  33704  rprmdvdsprod  34136  zarcmplem  34583  esumsnf  34766  satfv1lem  36294  eldm3  36704  rdgprc0  36733  bj-rdg0gALT  38177  zrdivrng  39079  disjresin  39367  eldioph4b  44011  diophren  44013  ismeannd  47682  psmeasure  47686  isomennd  47746  hoidmvlelem3  47812  stgr0  49263  tposres3  50199  setc1oid  50835  aacllem  51219