Theorem ima0 5174

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 4842	. 2 |- ( A " (/) ) = ran ( A |` (/) )
2		res0 5104	. . 3 |- ( A |` (/) ) = (/)
3	2	rneqi 5055	. 2 |- ran ( A |` (/) ) = ran (/)
4		rn0 5080	. 2 |- ran (/) = (/)
5	1, 3, 4	3eqtri 2459	1 |- ( A " (/) ) = (/)

Syntax hints:   = wceq 1364   (/)c0 3627   ran crn 4830   |` cres 4831   "cima 4832

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1671  ax-6 1709  ax-7 1729  ax-9 1761  ax-10 1776  ax-11 1781  ax-12 1793  ax-13 1944  ax-ext 2416  ax-sep 4403  ax-nul 4411  ax-pr 4521

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 962  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1702  df-eu 2260  df-mo 2261  df-clab 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-ne 2600  df-rab 2716  df-v 2966  df-dif 3321  df-un 3323  df-in 3325  df-ss 3332  df-nul 3628  df-if 3782  df-sn 3868  df-pr 3870  df-op 3874  df-br 4283  df-opab 4341  df-xp 4835  df-cnv 4837  df-dm 4839  df-rn 4840  df-res 4841  df-ima 4842

This theorem is referenced by:  csbima12  5176  relimasn  5182  elimasni  5186  dffv3  5677  supp0cosupp0  6719  imacosupp  6720  ecexr  7096  domunfican  7574  fodomfi  7580  efgrelexlema  16228  gsumval3OLD  16364  dprdsn  16509  cnindis  18740  cnhaus  18802  cmpfi  18855  xkouni  19016  xkoccn  19036  mbfima  20954  ismbf2d  20963  limcnlp  21197  mdeg0  21428  pserulm  21774  0pth  23294  spthispth  23297  1pthonlem2  23314  eupath2  23426  disjpreima  25754  imadifxp  25765  dstrvprob  26704  opelco3  27438  funpartlem  27822  inisegn0  29243