Theorem res0 5827

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 5536	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5618	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4114	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4287	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2785	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1538  Vcvv 3409   ∩ cin 3857  ∅c0 4225   × cxp 5522   ↾ cres 5526

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-ext 2729  ax-sep 5169  ax-nul 5176  ax-pr 5298

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-fal 1551  df-ex 1782  df-sb 2070  df-clab 2736  df-cleq 2750  df-clel 2830  df-rab 3079  df-v 3411  df-dif 3861  df-un 3863  df-in 3865  df-nul 4226  df-if 4421  df-sn 4523  df-pr 4525  df-op 4529  df-opab 5095  df-xp 5530  df-res 5536

This theorem is referenced by:  ima0  5917  resdisj  5998  smo0  8005  tfrlem16  8039  tz7.44-1  8052  mapunen  8708  fnfi  8829  ackbij2lem3  9701  hashf1lem1  13864  hashf1lem1OLD  13865  setsid  16596  meet0  17813  join0  17814  frmdplusg  18085  psgn0fv0  18706  gsum2dlem2  19159  ablfac1eulem  19262  ablfac1eu  19263  psrplusg  20709  ply1plusgfvi  20966  ptuncnv  22507  ptcmpfi  22513  ust0  22920  xrge0gsumle  23534  xrge0tsms  23535  jensen  25673  egrsubgr  27166  0grsubgr  27167  pthdlem1  27654  0pth  28009  1pthdlem1  28019  eupth2lemb  28121  fressupp  30546  resf1o  30589  xrge0tsmsd  30843  gsumle  30876  zarcmplem  31352  esumsnf  31551  satfv1lem  32840  dfpo2  33238  eldm3  33244  rdgprc0  33285  zrdivrng  35693  eldioph4b  40147  diophren  40149  ismeannd  43494  psmeasure  43498  isomennd  43558  hoidmvlelem3  43624  aacllem  45742