Theorem ima0 5202

Description: Image of the empty set. Theorem 3.16(ii) of [Monk1] p. 38. (Contributed by NM, 20-May-1998.)

Assertion

Ref	Expression
ima0	|- ( A " (/) ) = (/)

Proof of Theorem ima0

Step	Hyp	Ref	Expression
1		df-ima 4866	. 2 |- ( A " (/) ) = ran ( A |` (/) )
2		res0 5128	. . 3 |- ( A |` (/) ) = (/)
3	2	rneqi 5080	. 2 |- ran ( A |` (/) ) = ran (/)
4		rn0 5105	. 2 |- ran (/) = (/)
5	1, 3, 4	3eqtri 2488	1 |- ( A " (/) ) = (/)

Syntax hints:   = wceq 1455   (/)c0 3743   ran crn 4854   |` cres 4855   "cima 4856

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-9 1907  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442  ax-sep 4539  ax-nul 4548  ax-pr 4653

This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-3an 993  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-eu 2314  df-mo 2315  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-ne 2635  df-rab 2758  df-v 3059  df-dif 3419  df-un 3421  df-in 3423  df-ss 3430  df-nul 3744  df-if 3894  df-sn 3981  df-pr 3983  df-op 3987  df-br 4417  df-opab 4476  df-xp 4859  df-cnv 4861  df-dm 4863  df-rn 4864  df-res 4865  df-ima 4866

This theorem is referenced by:  csbima12  5204  relimasn  5210  elimasni  5214  inisegn0  5219  dffv3  5884  supp0cosupp0  6981  imacosupp  6982  ecexr  7394  domunfican  7870  fodomfi  7876  efgrelexlema  17448  dprdsn  17718  cnindis  20357  cnhaus  20419  cmpfi  20472  xkouni  20663  xkoccn  20683  mbfima  22637  ismbf2d  22646  limcnlp  22882  mdeg0  23068  pserulm  23426  0pth  25349  spthispth  25352  1pthonlem2  25369  eupath2  25757  disjpreima  28243  imadifxp  28261  dstrvprob  29353  opelco3  30469  funpartlem  30758  poimirlem1  31986  poimirlem2  31987  poimirlem3  31988  poimirlem4  31989  poimirlem5  31990  poimirlem6  31991  poimirlem7  31992  poimirlem10  31995  poimirlem11  31996  poimirlem12  31997  poimirlem13  31998  poimirlem16  32001  poimirlem17  32002  poimirlem19  32004  poimirlem20  32005  poimirlem22  32007  poimirlem23  32008  poimirlem24  32009  poimirlem25  32010  poimirlem28  32013  poimirlem29  32014  poimirlem31  32016  he0  36425  sPthisPth  39760  pthdlem2  39794  0pth-av  39841  1pthdlem2  39851