Theorem res0 5974

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 5663	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5750	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4163	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4345	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2788	1 ⊢ (𝐴 ↾ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1570  Vcvv 3451   ∩ cin 3898  ∅c0 4279   × cxp 5649   ↾ cres 5653

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 2733

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 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-in 3906  df-nul 4280  df-opab 5168  df-xp 5657  df-res 5663

This theorem is used by:  ima0  6071  resdisj  6160  dfpo2  6292  smo0  8350  tfrlem16  8385  tz7.44-1  8398  rdg0n  8426  mapunen  9149  fnfi  9177  ackbij2lem3  10299  hashf1lem1  14580  setsid  17365  join0  18557  meet0  18558  frmdplusg  19030  psgn0fv0  19705  gsum2dlem2  20165  ablfac1eulem  20268  ablfac1eu  20269  gsumle  20339  psrplusg  22225  ply1plusgfvi  22539  ptuncnv  24106  ptcmpfi  24112  ust0  24519  xrge0gsumle  25133  xrge0tsms  25134  jensen  27298  egrsubgr  29840  0grsubgr  29841  pthdlem1  30334  0pth  30698  1pthdlem1  30708  eupth2lemb  30820  fressupp  33263  resf1o  33304  xrge0tsmsd  33616  rprmdvdsprod  34048  zarcmplem  34495  esumsnf  34678  satfv1lem  36096  eldm3  36495  rdgprc0  36525  bj-rdg0gALT  37954  zrdivrng  38855  disjresin  39143  eldioph4b  43771  diophren  43773  ismeannd  47421  psmeasure  47425  isomennd  47485  hoidmvlelem3  47551  stgr0  49002  tposres3  49933  setc1oid  50547  aacllem  50883