Theorem res0 5389

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 5116	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5189	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 3803	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 3959	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2646	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1481  Vcvv 3195   ∩ cin 3566  ∅c0 3907   × cxp 5102   ↾ cres 5106

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600  ax-sep 4772  ax-nul 4780  ax-pr 4897

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1038  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-dif 3570  df-un 3572  df-in 3574  df-ss 3581  df-nul 3908  df-if 4078  df-sn 4169  df-pr 4171  df-op 4175  df-opab 4704  df-xp 5110  df-res 5116

This theorem is referenced by:  ima0  5469  resdisj  5551  smo0  7440  tfrlem16  7474  tz7.44-1  7487  mapunen  8114  fnfi  8223  ackbij2lem3  9048  hashf1lem1  13222  setsid  15895  meet0  17118  join0  17119  frmdplusg  17372  psgn0fv0  17912  gsum2dlem2  18351  ablfac1eulem  18452  ablfac1eu  18453  psrplusg  19362  ply1plusgfvi  19593  ptuncnv  21591  ptcmpfi  21597  ust0  22004  xrge0gsumle  22617  xrge0tsms  22618  jensen  24696  egrsubgr  26150  0grsubgr  26151  pthdlem1  26643  0pth  26966  1pthdlem1  26975  eupth2lemb  27077  resf1o  29479  gsumle  29753  xrge0tsmsd  29759  esumsnf  30100  dfpo2  31620  eldm3  31627  rdgprc0  31673  zrdivrng  33723  eldioph4b  37194  diophren  37196  ismeannd  40447  psmeasure  40451  isomennd  40508  hoidmvlelem3  40574  aacllem  42312