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 5662	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5749	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4114	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4344	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2787	1 ⊢ (𝐴 ↾ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1569  Vcvv 3450   ∩ cin 4089  ∅c0 4278   × cxp 5648   ↾ cres 5652

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 4047  df-in 4091  df-nul 4279  df-opab 5167  df-xp 5656  df-res 5662

This theorem is used by:  ima0  6074  resdisj  6160  dfpo2  6299  smo0  8369  tfrlem16  8404  tz7.44-1  8417  rdg0n  8445  mapunen  9168  fnfi  9196  ackbij2lem3  10321  hashf1lem1  14603  setsid  17390  join0  18582  meet0  18583  frmdplusg  19055  psgn0fv0  19730  gsum2dlem2  20190  ablfac1eulem  20293  ablfac1eu  20294  gsumle  20364  psrplusg  22250  ply1plusgfvi  22564  ptuncnv  24131  ptcmpfi  24137  ust0  24544  xrge0gsumle  25158  xrge0tsms  25159  jensen  27321  egrsubgr  29863  0grsubgr  29864  pthdlem1  30357  0pth  30721  1pthdlem1  30731  eupth2lemb  30843  fressupp  33328  resf1o  33368  xrge0tsmsd  33680  rprmdvdsprod  34112  zarcmplem  34559  esumsnf  34742  satfv1lem  36213  eldm3  36618  rdgprc0  36647  bj-rdg0gALT  38078  zrdivrng  38980  disjresin  39268  eldioph4b  43911  diophren  43913  ismeannd  47570  psmeasure  47574  isomennd  47634  hoidmvlelem3  47700  stgr0  49151  tposres3  50087  setc1oid  50723  aacllem  51107