Theorem res0 5980

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 5671	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5758	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4166	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4348	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2789	1 ⊢ (𝐴 ↾ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3453   ∩ cin 3901  ∅c0 4282   × cxp 5657   ↾ cres 5661

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3415  df-v 3455  df-dif 3905  df-in 3909  df-nul 4283  df-opab 5172  df-xp 5665  df-res 5671

This theorem is used by:  ima0  6077  resdisj  6166  dfpo2  6298  smo0  8351  tfrlem16  8386  tz7.44-1  8399  rdg0n  8427  mapunen  9148  fnfi  9176  ackbij2lem3  10246  hashf1lem1  14524  setsid  17305  join0  18497  meet0  18498  frmdplusg  18969  psgn0fv0  19644  gsum2dlem2  20104  ablfac1eulem  20207  ablfac1eu  20208  gsumle  20278  psrplusg  22158  ply1plusgfvi  22472  ptuncnv  24039  ptcmpfi  24045  ust0  24452  xrge0gsumle  25066  xrge0tsms  25067  jensen  27233  egrsubgr  29745  0grsubgr  29746  pthdlem1  30239  0pth  30603  1pthdlem1  30613  eupth2lemb  30725  fressupp  33168  resf1o  33209  xrge0tsmsd  33521  rprmdvdsprod  33952  zarcmplem  34399  esumsnf  34582  satfv1lem  35949  eldm3  36348  rdgprc0  36378  bj-rdg0gALT  37823  zrdivrng  38711  disjresin  38999  eldioph4b  43660  diophren  43662  ismeannd  47303  psmeasure  47307  isomennd  47367  hoidmvlelem3  47433  stgr0  48884  tposres3  49815  setc1oid  50429  aacllem  50780