Theorem res0 5954

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 5650	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5737	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4180	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4358	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2756	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1540  Vcvv 3447   ∩ cin 3913  ∅c0 4296   × cxp 5636   ↾ cres 5640

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701  ax-sep 5251  ax-nul 5261  ax-pr 5387

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-opab 5170  df-xp 5644  df-res 5650

This theorem is referenced by:  ima0  6048  resdisj  6142  dfpo2  6269  smo0  8327  tfrlem16  8361  tz7.44-1  8374  rdg0n  8402  mapunen  9110  fnfi  9142  ackbij2lem3  10193  hashf1lem1  14420  setsid  17177  join0  18364  meet0  18365  frmdplusg  18781  psgn0fv0  19441  gsum2dlem2  19901  ablfac1eulem  20004  ablfac1eu  20005  psrplusg  21845  ply1plusgfvi  22126  ptuncnv  23694  ptcmpfi  23700  ust0  24107  xrge0gsumle  24722  xrge0tsms  24723  jensen  26899  egrsubgr  29204  0grsubgr  29205  pthdlem1  29696  0pth  30054  1pthdlem1  30064  eupth2lemb  30166  fressupp  32611  resf1o  32653  xrge0tsmsd  33002  gsumle  33038  rprmdvdsprod  33505  zarcmplem  33871  esumsnf  34054  satfv1lem  35349  eldm3  35748  rdgprc0  35781  bj-rdg0gALT  37059  zrdivrng  37947  disjresin  38228  eldioph4b  42799  diophren  42801  ismeannd  46465  psmeasure  46469  isomennd  46529  hoidmvlelem3  46595  stgr0  47959  tposres3  48869  setc1oid  49484  aacllem  49790