Theorem ima0 6036

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 5638	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5942	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5886	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5875	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2767	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1547  ∅c0 4268  ran crn 5626   ↾ cres 5627   “ cima 5628

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2712  ax-sep 5225  ax-pr 5369

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2719  df-cleq 2732  df-clel 2815  df-rab 3393  df-v 3434  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4269  df-if 4462  df-sn 4563  df-pr 4565  df-op 4569  df-br 5080  df-opab 5142  df-xp 5631  df-cnv 5633  df-dm 5635  df-rn 5636  df-res 5637  df-ima 5638

This theorem is referenced by:  csbima12  6038  relimasn  6044  elimasni  6050  inisegn0  6057  predprc  6296  dffv3  6830  suppco  8153  supp0cosupp0  8155  ecexr  8645  fodomfi  9219  imafiOLD  9223  domunfican  9229  fodomfiOLD  9237  efgrelexlema  19722  dprdsn  20011  cnindis  23282  cnhaus  23344  cmpfi  23398  xkouni  23589  xkoccn  23609  mbfima  25622  ismbf2d  25632  limcnlp  25870  mdeg0  26060  pserulm  26412  old0  27856  made0  27880  neg0s  28043  neg1s  28044  zcuts0  28425  spthispth  29817  dfpth2  29822  pthdlem2  29861  0pth  30220  1pthdlem2  30231  eupth2lemb  30332  disjpreima  32680  imadifxp  32697  2ndimaxp  32745  mptiffisupp  32792  swrdrndisj  33043  gsumpart  33151  esplyfval2  33756  zarclsint  34063  dstrvprob  34663  opelco3  36010  funpartlem  36177  poimirlem1  37995  poimirlem2  37996  poimirlem3  37997  poimirlem4  37998  poimirlem5  37999  poimirlem6  38000  poimirlem7  38001  poimirlem10  38004  poimirlem11  38005  poimirlem12  38006  poimirlem13  38007  poimirlem16  38010  poimirlem17  38011  poimirlem19  38013  poimirlem20  38014  poimirlem22  38016  poimirlem23  38017  poimirlem24  38018  poimirlem25  38019  poimirlem28  38022  poimirlem29  38023  poimirlem31  38025  he0  44235  smfresal  47238  predisj  49308