Theorem ima0 5295

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 4964	. 2 |- ( A " (/) ) = ran ( A |` (/) )
2		res0 5226	. . 3 |- ( A |` (/) ) = (/)
3	2	rneqi 5177	. 2 |- ran ( A |` (/) ) = ran (/)
4		rn0 5202	. 2 |- ran (/) = (/)
5	1, 3, 4	3eqtri 2487	1 |- ( A " (/) ) = (/)

Syntax hints:   = wceq 1370   (/)c0 3748   ran crn 4952   |` cres 4953   "cima 4954

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-9 1762  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432  ax-sep 4524  ax-nul 4532  ax-pr 4642

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-eu 2266  df-mo 2267  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ne 2650  df-rab 2808  df-v 3080  df-dif 3442  df-un 3444  df-in 3446  df-ss 3453  df-nul 3749  df-if 3903  df-sn 3989  df-pr 3991  df-op 3995  df-br 4404  df-opab 4462  df-xp 4957  df-cnv 4959  df-dm 4961  df-rn 4962  df-res 4963  df-ima 4964

This theorem is referenced by:  csbima12  5297  relimasn  5303  elimasni  5307  dffv3  5798  supp0cosupp0  6841  imacosupp  6842  ecexr  7219  domunfican  7698  fodomfi  7704  efgrelexlema  16371  gsumval3OLD  16507  dprdsn  16665  cnindis  19038  cnhaus  19100  cmpfi  19153  xkouni  19314  xkoccn  19334  mbfima  21253  ismbf2d  21262  limcnlp  21496  mdeg0  21684  pserulm  22030  0pth  23648  spthispth  23651  1pthonlem2  23668  eupath2  23780  disjpreima  26106  imadifxp  26117  dstrvprob  27021  opelco3  27756  funpartlem  28140  inisegn0  29567