Theorem ima0 5912

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 5532	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5822	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5771	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5760	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2825	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1538  ∅c0 4243  ran crn 5520   ↾ cres 5521   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770  ax-sep 5167  ax-nul 5174  ax-pr 5295

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-mo 2598  df-eu 2629  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-dif 3884  df-un 3886  df-in 3888  df-ss 3898  df-nul 4244  df-if 4426  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  csbima12  5914  relimasn  5919  elimasni  5923  inisegn0  5928  dffv3  6641  suppco  7853  supp0cosupp0  7855  supp0cosupp0OLD  7856  imacosuppOLD  7858  ecexr  8277  domunfican  8775  fodomfi  8781  efgrelexlema  18867  dprdsn  19151  cnindis  21897  cnhaus  21959  cmpfi  22013  xkouni  22204  xkoccn  22224  mbfima  24234  ismbf2d  24244  limcnlp  24481  mdeg0  24671  pserulm  25017  spthispth  27515  pthdlem2  27557  0pth  27910  1pthdlem2  27921  eupth2lemb  28022  disjpreima  30347  imadifxp  30364  2ndimaxp  30409  swrdrndisj  30657  gsumpart  30740  zarclsint  31225  dstrvprob  31839  opelco3  33131  funpartlem  33516  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem22  35079  poimirlem23  35080  poimirlem24  35081  poimirlem25  35082  poimirlem28  35085  poimirlem29  35086  poimirlem31  35088  he0  40485  smfresal  43420