Theorem res0 5400

Description: A restriction to the empty set is empty. (Contributed by NM, 12-Nov-1994.)

Assertion

Ref	Expression
res0	|- ( A |` (/) ) = (/)

Proof of Theorem res0

Step	Hyp	Ref	Expression
1		df-res 5126	. 2 |- ( A |` (/) ) = ( A i^i ( (/) X. _V ) )
2		0xp 5199	. . 3 |- ( (/) X. _V ) = (/)
3	2	ineq2i 3811	. 2 |- ( A i^i ( (/) X. _V ) ) = ( A i^i (/) )
4		in0 3968	. 2 |- ( A i^i (/) ) = (/)
5	1, 3, 4	3eqtri 2648	1 |- ( A |` (/) ) = (/)

Syntax hints:   = wceq 1483   _Vcvv 3200   i^i cin 3573   (/)c0 3915   X. cxp 5112   |` cres 5116

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602  ax-sep 4781  ax-nul 4789  ax-pr 4906

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-3an 1039  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-dif 3577  df-un 3579  df-in 3581  df-ss 3588  df-nul 3916  df-if 4087  df-sn 4178  df-pr 4180  df-op 4184  df-opab 4713  df-xp 5120  df-res 5126

This theorem is referenced by:  ima0  5481  resdisj  5563  smo0  7455  tfrlem16  7489  tz7.44-1  7502  mapunen  8129  fnfi  8238  ackbij2lem3  9063  hashf1lem1  13239  setsid  15914  meet0  17137  join0  17138  frmdplusg  17391  psgn0fv0  17931  gsum2dlem2  18370  ablfac1eulem  18471  ablfac1eu  18472  psrplusg  19381  ply1plusgfvi  19612  ptuncnv  21610  ptcmpfi  21616  ust0  22023  xrge0gsumle  22636  xrge0tsms  22637  jensen  24715  egrsubgr  26169  0grsubgr  26170  pthdlem1  26662  0pth  26986  1pthdlem1  26995  eupth2lemb  27097  resf1o  29505  gsumle  29779  xrge0tsmsd  29785  esumsnf  30126  dfpo2  31645  eldm3  31651  rdgprc0  31699  zrdivrng  33752  eldioph4b  37375  diophren  37377  ismeannd  40684  psmeasure  40688  isomennd  40745  hoidmvlelem3  40811  aacllem  42547