Theorem ima0 6070

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

Assertion

Ref	Expression
ima0	⊢ (𝐴 “ ∅) = ∅

Proof of Theorem ima0

Step	Hyp	Ref	Expression
1		df-ima 5665	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5973	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5918	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5907	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2792	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1563  ∅c0 4288  ran crn 5653   ↾ cres 5654   “ cima 5655

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737  ax-sep 5251  ax-pr 5395

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1566  df-fal 1576  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3418  df-v 3459  df-dif 3910  df-un 3912  df-in 3914  df-ss 3924  df-nul 4289  df-if 4484  df-sn 4586  df-pr 4588  df-op 4592  df-br 5106  df-opab 5168  df-xp 5658  df-cnv 5660  df-dm 5662  df-rn 5663  df-res 5664  df-ima 5665

This theorem is referenced by:  csbima12  6072  relimasn  6078  elimasni  6084  inisegn0  6091  predprc  6329  dffv3  6867  suppco  8190  supp0cosupp0  8192  ecexr  8687  fodomfi  9260  domunfican  9269  efgrelexlema  19810  dprdsn  20099  cnindis  23410  cnhaus  23472  cmpfi  23526  xkouni  23717  xkoccn  23737  mbfima  25750  ismbf2d  25760  limcnlp  25998  mdeg0  26188  pserulm  26543  old0  27990  made0  28014  neg0s  28177  neg1s  28178  zcuts0  28559  spthispth  29982  dfpth2  29987  pthdlem2  30026  0pth  30385  1pthdlem2  30396  eupth2lemb  30497  disjpreima  32839  imadifxp  32856  2ndimaxp  32903  mptiffisupp  32950  swrdrndisj  33190  gsumpart  33296  esplyfval2  33872  zarclsint  34179  dstrvprob  34779  opelco3  36138  funpartlem  36305  poimirlem1  38132  poimirlem2  38133  poimirlem3  38134  poimirlem4  38135  poimirlem5  38136  poimirlem6  38137  poimirlem7  38138  poimirlem10  38141  poimirlem11  38142  poimirlem12  38143  poimirlem13  38144  poimirlem16  38147  poimirlem17  38148  poimirlem19  38150  poimirlem20  38151  poimirlem22  38153  poimirlem23  38154  poimirlem24  38155  poimirlem25  38156  poimirlem28  38159  poimirlem29  38160  poimirlem31  38162  he0  44372  smfresal  47360  predisj  49440