Theorem res0 5932

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 5628	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5715	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4167	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4345	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2758	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1541  Vcvv 3436   ∩ cin 3901  ∅c0 4283   × cxp 5614   ↾ cres 5618

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 2113  ax-9 2121  ax-ext 2703  ax-sep 5234  ax-nul 5244  ax-pr 5370

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4476  df-sn 4577  df-pr 4579  df-op 4583  df-opab 5154  df-xp 5622  df-res 5628

This theorem is referenced by:  ima0  6026  resdisj  6116  dfpo2  6243  smo0  8278  tfrlem16  8312  tz7.44-1  8325  rdg0n  8353  mapunen  9059  fnfi  9087  ackbij2lem3  10131  hashf1lem1  14362  setsid  17118  join0  18309  meet0  18310  frmdplusg  18762  psgn0fv0  19424  gsum2dlem2  19884  ablfac1eulem  19987  ablfac1eu  19988  gsumle  20058  psrplusg  21874  ply1plusgfvi  22155  ptuncnv  23723  ptcmpfi  23729  ust0  24136  xrge0gsumle  24750  xrge0tsms  24751  jensen  26927  egrsubgr  29256  0grsubgr  29257  pthdlem1  29745  0pth  30103  1pthdlem1  30113  eupth2lemb  30215  fressupp  32667  resf1o  32711  xrge0tsmsd  33040  rprmdvdsprod  33497  zarcmplem  33892  esumsnf  34075  satfv1lem  35404  eldm3  35803  rdgprc0  35833  bj-rdg0gALT  37111  zrdivrng  37999  disjresin  38280  eldioph4b  42850  diophren  42852  ismeannd  46511  psmeasure  46515  isomennd  46575  hoidmvlelem3  46641  stgr0  47997  tposres3  48918  setc1oid  49533  aacllem  49839