Theorem res0 5942

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 5636	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5723	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4169	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4347	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2763	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1541  Vcvv 3440   ∩ cin 3900  ∅c0 4285   × cxp 5622   ↾ cres 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-in 3908  df-nul 4286  df-opab 5161  df-xp 5630  df-res 5636

This theorem is referenced by:  ima0  6036  resdisj  6127  dfpo2  6254  smo0  8290  tfrlem16  8324  tz7.44-1  8337  rdg0n  8365  mapunen  9074  fnfi  9102  ackbij2lem3  10150  hashf1lem1  14378  setsid  17134  join0  18326  meet0  18327  frmdplusg  18779  psgn0fv0  19440  gsum2dlem2  19900  ablfac1eulem  20003  ablfac1eu  20004  gsumle  20074  psrplusg  21892  ply1plusgfvi  22182  ptuncnv  23751  ptcmpfi  23757  ust0  24164  xrge0gsumle  24778  xrge0tsms  24779  jensen  26955  egrsubgr  29350  0grsubgr  29351  pthdlem1  29839  0pth  30200  1pthdlem1  30210  eupth2lemb  30312  fressupp  32767  resf1o  32809  xrge0tsmsd  33155  rprmdvdsprod  33615  zarcmplem  34038  esumsnf  34221  satfv1lem  35556  eldm3  35955  rdgprc0  35985  bj-rdg0gALT  37272  zrdivrng  38150  disjresin  38435  eldioph4b  43049  diophren  43051  ismeannd  46707  psmeasure  46711  isomennd  46771  hoidmvlelem3  46837  stgr0  48202  tposres3  49122  setc1oid  49736  aacllem  50042