Theorem ima0 6097

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 5702	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 6004	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5951	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5939	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2767	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1537  ∅c0 4339  ran crn 5690   ↾ cres 5691   “ cima 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-10 2139  ax-11 2155  ax-12 2175  ax-ext 2706  ax-sep 5302  ax-nul 5312  ax-pr 5438

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-nf 1781  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-xp 5695  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702

This theorem is referenced by:  csbima12  6099  relimasn  6105  elimasni  6112  inisegn0  6119  predprc  6361  dffv3  6903  suppco  8230  supp0cosupp0  8232  ecexr  8749  fodomfi  9348  imafiOLD  9352  domunfican  9359  fodomfiOLD  9368  efgrelexlema  19782  dprdsn  20071  cnindis  23316  cnhaus  23378  cmpfi  23432  xkouni  23623  xkoccn  23643  mbfima  25679  ismbf2d  25689  limcnlp  25928  mdeg0  26124  pserulm  26480  old0  27913  made0  27927  negs0s  28073  negs1s  28074  spthispth  29759  pthdlem2  29801  0pth  30154  1pthdlem2  30165  eupth2lemb  30266  disjpreima  32604  imadifxp  32621  2ndimaxp  32663  mptiffisupp  32708  swrdrndisj  32927  gsumpart  33043  zarclsint  33833  dstrvprob  34453  opelco3  35756  funpartlem  35924  poimirlem1  37608  poimirlem2  37609  poimirlem3  37610  poimirlem4  37611  poimirlem5  37612  poimirlem6  37613  poimirlem7  37614  poimirlem10  37617  poimirlem11  37618  poimirlem12  37619  poimirlem13  37620  poimirlem16  37623  poimirlem17  37624  poimirlem19  37626  poimirlem20  37627  poimirlem22  37629  poimirlem23  37630  poimirlem24  37631  poimirlem25  37632  poimirlem28  37635  poimirlem29  37636  poimirlem31  37638  he0  43774  smfresal  46744  predisj  48659