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

Syntax hints:   = wceq 1541  ∅c0 4285  ran crn 5625   ↾ cres 5626   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708  ax-sep 5241  ax-nul 5251  ax-pr 5377

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  csbima12  6038  relimasn  6044  elimasni  6050  inisegn0  6057  predprc  6296  dffv3  6830  suppco  8148  supp0cosupp0  8150  ecexr  8640  fodomfi  9212  imafiOLD  9216  domunfican  9222  fodomfiOLD  9230  efgrelexlema  19678  dprdsn  19967  cnindis  23236  cnhaus  23298  cmpfi  23352  xkouni  23543  xkoccn  23563  mbfima  25587  ismbf2d  25597  limcnlp  25835  mdeg0  26031  pserulm  26387  old0  27835  made0  27859  neg0s  28022  neg1s  28023  zcuts0  28404  spthispth  29797  dfpth2  29802  pthdlem2  29841  0pth  30200  1pthdlem2  30211  eupth2lemb  30312  disjpreima  32659  imadifxp  32676  2ndimaxp  32724  mptiffisupp  32772  swrdrndisj  33039  gsumpart  33146  esplyfval2  33723  zarclsint  34029  dstrvprob  34629  opelco3  35969  funpartlem  36136  poimirlem1  37818  poimirlem2  37819  poimirlem3  37820  poimirlem4  37821  poimirlem5  37822  poimirlem6  37823  poimirlem7  37824  poimirlem10  37827  poimirlem11  37828  poimirlem12  37829  poimirlem13  37830  poimirlem16  37833  poimirlem17  37834  poimirlem19  37836  poimirlem20  37837  poimirlem22  37839  poimirlem23  37840  poimirlem24  37841  poimirlem25  37842  poimirlem28  37845  poimirlem29  37846  poimirlem31  37848  he0  44021  smfresal  47028  predisj  49052