Theorem res0 5967

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 5657	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5744	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4169	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4348	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2788	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1559  Vcvv 3453   ∩ cin 3903  ∅c0 4285   × cxp 5643   ↾ cres 5647

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-in 3911  df-nul 4286  df-opab 5162  df-xp 5651  df-res 5657

This theorem is referenced by:  ima0  6063  resdisj  6151  dfpo2  6279  smo0  8324  tfrlem16  8359  tz7.44-1  8372  rdg0n  8400  mapunen  9114  fnfi  9142  ackbij2lem3  10193  hashf1lem1  14465  setsid  17226  join0  18418  meet0  18419  frmdplusg  18871  psgn0fv0  19534  gsum2dlem2  19994  ablfac1eulem  20097  ablfac1eu  20098  gsumle  20168  psrplusg  21969  ply1plusgfvi  22283  ptuncnv  23847  ptcmpfi  23853  ust0  24260  xrge0gsumle  24874  xrge0tsms  24875  jensen  27030  egrsubgr  29424  0grsubgr  29425  pthdlem1  29912  0pth  30273  1pthdlem1  30283  eupth2lemb  30385  fressupp  32840  resf1o  32882  xrge0tsmsd  33214  rprmdvdsprod  33691  zarcmplem  34139  esumsnf  34322  satfv1lem  35676  eldm3  36075  rdgprc0  36105  bj-rdg0gALT  37520  zrdivrng  38416  disjresin  38706  eldioph4b  43352  diophren  43354  ismeannd  47005  psmeasure  47009  isomennd  47069  hoidmvlelem3  47135  stgr0  48546  tposres3  49466  setc1oid  50080  aacllem  50386