Theorem res0 5538

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 5261	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5339	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 3962	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4112	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2797	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1631  Vcvv 3351   ∩ cin 3722  ∅c0 4063   × cxp 5247   ↾ cres 5251

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4915  ax-nul 4923  ax-pr 5034

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-opab 4847  df-xp 5255  df-res 5261

This theorem is referenced by:  ima0  5622  resdisj  5704  smo0  7608  tfrlem16  7642  tz7.44-1  7655  mapunen  8285  fnfi  8394  ackbij2lem3  9265  hashf1lem1  13441  setsid  16121  meet0  17345  join0  17346  frmdplusg  17599  psgn0fv0  18138  gsum2dlem2  18577  ablfac1eulem  18679  ablfac1eu  18680  psrplusg  19596  ply1plusgfvi  19827  ptuncnv  21831  ptcmpfi  21837  ust0  22243  xrge0gsumle  22856  xrge0tsms  22857  jensen  24936  egrsubgr  26392  0grsubgr  26393  pthdlem1  26897  0pth  27305  1pthdlem1  27315  eupth2lemb  27417  resf1o  29845  gsumle  30119  xrge0tsmsd  30125  esumsnf  30466  dfpo2  31983  eldm3  31989  rdgprc0  32035  zrdivrng  34084  eldioph4b  37901  diophren  37903  ismeannd  41201  psmeasure  41205  isomennd  41265  hoidmvlelem3  41331  aacllem  43078