Theorem res0 5993

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 5694	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5780	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4211	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4395	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2760	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1533  Vcvv 3473   ∩ cin 3948  ∅c0 4326   × cxp 5680   ↾ cres 5684

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-ext 2699  ax-sep 5303  ax-nul 5310  ax-pr 5433

This theorem depends on definitions:  df-bi 206  df-an 395  df-or 846  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-sb 2060  df-clab 2706  df-cleq 2720  df-clel 2806  df-rab 3431  df-v 3475  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4327  df-if 4533  df-sn 4633  df-pr 4635  df-op 4639  df-opab 5215  df-xp 5688  df-res 5694

This theorem is referenced by:  ima0  6085  resdisj  6178  dfpo2  6305  smo0  8385  tfrlem16  8420  tz7.44-1  8433  rdg0n  8461  mapunen  9177  fnfi  9212  ackbij2lem3  10272  hashf1lem1  14455  hashf1lem1OLD  14456  setsid  17184  join0  18404  meet0  18405  frmdplusg  18813  psgn0fv0  19473  gsum2dlem2  19933  ablfac1eulem  20036  ablfac1eu  20037  psrplusg  21888  ply1plusgfvi  22167  ptuncnv  23731  ptcmpfi  23737  ust0  24144  xrge0gsumle  24769  xrge0tsms  24770  jensen  26941  egrsubgr  29110  0grsubgr  29111  pthdlem1  29600  0pth  29955  1pthdlem1  29965  eupth2lemb  30067  fressupp  32489  resf1o  32533  xrge0tsmsd  32792  gsumle  32825  rprmdvdsprod  33273  zarcmplem  33515  esumsnf  33716  satfv1lem  35005  eldm3  35388  rdgprc0  35422  bj-rdg0gALT  36583  zrdivrng  37459  disjresin  37743  eldioph4b  42262  diophren  42264  ismeannd  45884  psmeasure  45888  isomennd  45948  hoidmvlelem3  46014  aacllem  48312

Otomatik - 173.255.232.114 CloudFlare DNS Türk Telekom DNS Google DNS Open DNS

OSZAR »