Theorem res0 5946

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 5735	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4174	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4356	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2763	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1541  Vcvv 3446   ∩ cin 3912  ∅c0 4287   × cxp 5636   ↾ cres 5640

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-opab 5173  df-xp 5644  df-res 5650

This theorem is referenced by:  ima0  6034  resdisj  6126  dfpo2  6253  smo0  8309  tfrlem16  8344  tz7.44-1  8357  rdg0n  8385  mapunen  9097  fnfi  9132  ackbij2lem3  10186  hashf1lem1  14365  hashf1lem1OLD  14366  setsid  17091  join0  18308  meet0  18309  frmdplusg  18678  psgn0fv0  19307  gsum2dlem2  19762  ablfac1eulem  19865  ablfac1eu  19866  psrplusg  21386  ply1plusgfvi  21650  ptuncnv  23195  ptcmpfi  23201  ust0  23608  xrge0gsumle  24233  xrge0tsms  24234  jensen  26375  egrsubgr  28288  0grsubgr  28289  pthdlem1  28777  0pth  29132  1pthdlem1  29142  eupth2lemb  29244  fressupp  31670  resf1o  31715  xrge0tsmsd  31969  gsumle  32002  zarcmplem  32551  esumsnf  32752  satfv1lem  34043  eldm3  34420  rdgprc0  34454  bj-rdg0gALT  35615  zrdivrng  36485  disjresin  36770  eldioph4b  41192  diophren  41194  ismeannd  44828  psmeasure  44832  isomennd  44892  hoidmvlelem3  44958  aacllem  47368