Theorem res0 5985

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 5688	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5774	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4209	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4391	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2763	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1540  Vcvv 3473   ∩ cin 3947  ∅c0 4322   × cxp 5674   ↾ cres 5678

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 1912  ax-6 1970  ax-7 2010  ax-8 2107  ax-9 2115  ax-ext 2702  ax-sep 5299  ax-nul 5306  ax-pr 5427

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1781  df-sb 2067  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3432  df-v 3475  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-opab 5211  df-xp 5682  df-res 5688

This theorem is referenced by:  ima0  6076  resdisj  6168  dfpo2  6295  smo0  8364  tfrlem16  8399  tz7.44-1  8412  rdg0n  8440  mapunen  9152  fnfi  9187  ackbij2lem3  10242  hashf1lem1  14422  hashf1lem1OLD  14423  setsid  17148  join0  18368  meet0  18369  frmdplusg  18777  psgn0fv0  19427  gsum2dlem2  19887  ablfac1eulem  19990  ablfac1eu  19991  psrplusg  21810  ply1plusgfvi  22084  ptuncnv  23631  ptcmpfi  23637  ust0  24044  xrge0gsumle  24669  xrge0tsms  24670  jensen  26835  egrsubgr  28968  0grsubgr  28969  pthdlem1  29457  0pth  29812  1pthdlem1  29822  eupth2lemb  29924  fressupp  32344  resf1o  32389  xrge0tsmsd  32646  gsumle  32679  zarcmplem  33326  esumsnf  33527  satfv1lem  34818  eldm3  35202  rdgprc0  35236  bj-rdg0gALT  36418  zrdivrng  37287  disjresin  37572  eldioph4b  42014  diophren  42016  ismeannd  45644  psmeasure  45648  isomennd  45708  hoidmvlelem3  45774  aacllem  48012