Theorem ima0 5357

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 5017	. 2 |- ( A " (/) ) = ran ( A |` (/) )
2		res0 5283	. . 3 |- ( A |` (/) ) = (/)
3	2	rneqi 5234	. 2 |- ran ( A |` (/) ) = ran (/)
4		rn0 5259	. 2 |- ran (/) = (/)
5	1, 3, 4	3eqtri 2500	1 |- ( A " (/) ) = (/)

Syntax hints:   = wceq 1379   (/)c0 3790   ran crn 5005   |` cres 5006   "cima 5007

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-9 1771  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-eu 2279  df-mo 2280  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ne 2664  df-rab 2826  df-v 3120  df-dif 3484  df-un 3486  df-in 3488  df-ss 3495  df-nul 3791  df-if 3945  df-sn 4033  df-pr 4035  df-op 4039  df-br 4453  df-opab 4511  df-xp 5010  df-cnv 5012  df-dm 5014  df-rn 5015  df-res 5016  df-ima 5017

This theorem is referenced by:  csbima12  5359  relimasn  5365  elimasni  5369  dffv3  5867  supp0cosupp0  6949  imacosupp  6950  ecexr  7326  domunfican  7803  fodomfi  7809  efgrelexlema  16617  gsumval3OLD  16758  dprdsn  16932  cnindis  19638  cnhaus  19700  cmpfi  19753  xkouni  19945  xkoccn  19965  mbfima  21884  ismbf2d  21893  limcnlp  22127  mdeg0  22315  pserulm  22661  0pth  24363  spthispth  24366  1pthonlem2  24383  eupath2  24771  disjpreima  27236  imadifxp  27249  dstrvprob  28203  opelco3  29103  funpartlem  29487  inisegn0  30885