Theorem ima0 6044

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 5645	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5950	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5894	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5883	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2764	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1542  ∅c0 4287  ran crn 5633   ↾ cres 5634   “ cima 5635

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709  ax-sep 5243  ax-pr 5379

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  csbima12  6046  relimasn  6052  elimasni  6058  inisegn0  6065  predprc  6304  dffv3  6838  suppco  8158  supp0cosupp0  8160  ecexr  8650  fodomfi  9224  imafiOLD  9228  domunfican  9234  fodomfiOLD  9242  efgrelexlema  19690  dprdsn  19979  cnindis  23248  cnhaus  23310  cmpfi  23364  xkouni  23555  xkoccn  23575  mbfima  25599  ismbf2d  25609  limcnlp  25847  mdeg0  26043  pserulm  26399  old0  27847  made0  27871  neg0s  28034  neg1s  28035  zcuts0  28416  spthispth  29809  dfpth2  29814  pthdlem2  29853  0pth  30212  1pthdlem2  30223  eupth2lemb  30324  disjpreima  32670  imadifxp  32687  2ndimaxp  32735  mptiffisupp  32782  swrdrndisj  33049  gsumpart  33156  esplyfval2  33741  zarclsint  34049  dstrvprob  34649  opelco3  35988  funpartlem  36155  poimirlem1  37866  poimirlem2  37867  poimirlem3  37868  poimirlem4  37869  poimirlem5  37870  poimirlem6  37871  poimirlem7  37872  poimirlem10  37875  poimirlem11  37876  poimirlem12  37877  poimirlem13  37878  poimirlem16  37881  poimirlem17  37882  poimirlem19  37884  poimirlem20  37885  poimirlem22  37887  poimirlem23  37888  poimirlem24  37889  poimirlem25  37890  poimirlem28  37893  poimirlem29  37894  poimirlem31  37896  he0  44134  smfresal  47140  predisj  49164