Theorem ima0 6095

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 5698	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 6001	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5948	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5936	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2769	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4333  ran crn 5686   ↾ cres 5687   “ cima 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2708  ax-sep 5296  ax-nul 5306  ax-pr 5432

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-xp 5691  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by:  csbima12  6097  relimasn  6103  elimasni  6109  inisegn0  6116  predprc  6359  dffv3  6902  suppco  8231  supp0cosupp0  8233  ecexr  8750  fodomfi  9350  imafiOLD  9354  domunfican  9361  fodomfiOLD  9370  efgrelexlema  19767  dprdsn  20056  cnindis  23300  cnhaus  23362  cmpfi  23416  xkouni  23607  xkoccn  23627  mbfima  25665  ismbf2d  25675  limcnlp  25913  mdeg0  26109  pserulm  26465  old0  27898  made0  27912  negs0s  28058  negs1s  28059  spthispth  29744  dfpth2  29749  pthdlem2  29788  0pth  30144  1pthdlem2  30155  eupth2lemb  30256  disjpreima  32597  imadifxp  32614  2ndimaxp  32656  mptiffisupp  32702  swrdrndisj  32942  gsumpart  33060  zarclsint  33871  dstrvprob  34474  opelco3  35775  funpartlem  35943  poimirlem1  37628  poimirlem2  37629  poimirlem3  37630  poimirlem4  37631  poimirlem5  37632  poimirlem6  37633  poimirlem7  37634  poimirlem10  37637  poimirlem11  37638  poimirlem12  37639  poimirlem13  37640  poimirlem16  37643  poimirlem17  37644  poimirlem19  37646  poimirlem20  37647  poimirlem22  37649  poimirlem23  37650  poimirlem24  37651  poimirlem25  37652  poimirlem28  37655  poimirlem29  37656  poimirlem31  37658  he0  43797  smfresal  46803  predisj  48730