Theorem res0 5605

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 5325	. 2 ⊢ (𝐴 ↾ ∅) = (𝐴 ∩ (∅ × V))
2		0xp 5405	. . 3 ⊢ (∅ × V) = ∅
3	2	ineq2i 4010	. 2 ⊢ (𝐴 ∩ (∅ × V)) = (𝐴 ∩ ∅)
4		in0 4165	. 2 ⊢ (𝐴 ∩ ∅) = ∅
5	1, 3, 4	3eqtri 2826	1 ⊢ (𝐴 ↾ ∅) = ∅

Syntax hints:   = wceq 1653  Vcvv 3386   ∩ cin 3769  ∅c0 4116   × cxp 5311   ↾ cres 5315

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2378  ax-ext 2778  ax-sep 4976  ax-nul 4984  ax-pr 5098

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2787  df-cleq 2793  df-clel 2796  df-nfc 2931  df-v 3388  df-dif 3773  df-un 3775  df-in 3777  df-ss 3784  df-nul 4117  df-if 4279  df-sn 4370  df-pr 4372  df-op 4376  df-opab 4907  df-xp 5319  df-res 5325

This theorem is referenced by:  ima0  5699  resdisj  5781  smo0  7695  tfrlem16  7729  tz7.44-1  7742  mapunen  8372  fnfi  8481  ackbij2lem3  9352  hashf1lem1  13487  setsid  16238  meet0  17451  join0  17452  frmdplusg  17706  psgn0fv0  18243  gsum2dlem2  18684  ablfac1eulem  18786  ablfac1eu  18787  psrplusg  19703  ply1plusgfvi  19933  ptuncnv  21938  ptcmpfi  21944  ust0  22350  xrge0gsumle  22963  xrge0tsms  22964  jensen  25066  egrsubgr  26510  0grsubgr  26511  pthdlem1  27019  0pth  27468  1pthdlem1  27478  eupth2lemb  27581  resf1o  30022  gsumle  30294  xrge0tsmsd  30300  esumsnf  30641  dfpo2  32158  eldm3  32164  rdgprc0  32210  zrdivrng  34238  eldioph4b  38156  diophren  38158  ismeannd  41422  psmeasure  41426  isomennd  41486  hoidmvlelem3  41552  aacllem  43344