Theorem ima0 6084

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 5679	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5987	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5932	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5921	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2793	1 ⊢ (𝐴 “ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4289  ran crn 5667   ↾ cres 5668   “ cima 5669

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2738  ax-sep 5262  ax-pr 5409

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2745  df-cleq 2758  df-clel 2841  df-rab 3420  df-v 3460  df-dif 3911  df-un 3913  df-in 3915  df-ss 3925  df-nul 4290  df-if 4493  df-sn 4595  df-pr 4597  df-op 4601  df-br 5115  df-opab 5179  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is used by:  csbima12  6086  relimasn  6092  elimasni  6098  inisegn0  6105  predprc  6346  dffv3  6884  suppco  8211  supp0cosupp0  8213  ecexr  8708  fodomfi  9282  domunfican  9291  efgrelexlema  19850  dprdsn  20139  cnindis  23486  cnhaus  23548  cmpfi  23602  xkouni  23793  xkoccn  23813  mbfima  25826  ismbf2d  25836  limcnlp  26074  mdeg0  26264  pserulm  26622  old0  28069  made0  28093  neg0s  28256  neg1s  28257  zcuts0  28638  spthispth  30110  dfpth2  30115  pthdlem2  30154  0pth  30513  1pthdlem2  30524  eupth2lemb  30625  disjpreima  32966  imadifxp  32983  2ndimaxp  33028  mptiffisupp  33075  swrdrndisj  33308  gsumpart  33414  esplyfval2  33986  zarclsint  34293  dstrvprob  34894  opelco3  36288  funpartlem  36455  poimirlem1  38313  poimirlem2  38314  poimirlem3  38315  poimirlem4  38316  poimirlem5  38317  poimirlem6  38318  poimirlem7  38319  poimirlem10  38322  poimirlem11  38323  poimirlem12  38324  poimirlem13  38325  poimirlem16  38328  poimirlem17  38329  poimirlem19  38331  poimirlem20  38332  poimirlem22  38334  poimirlem23  38335  poimirlem24  38336  poimirlem25  38337  poimirlem28  38340  poimirlem29  38341  poimirlem31  38343  he0  44551  smfresal  47543  predisj  49630