Theorem ima0 6081

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 5676	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5984	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5929	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5918	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2790	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1570  ∅c0 4287  ran crn 5664   ↾ cres 5665   “ cima 5666

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735  ax-sep 5258  ax-pr 5406

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4288  df-if 4489  df-sn 4591  df-pr 4593  df-op 4597  df-br 5111  df-opab 5175  df-xp 5669  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is referenced by:  csbima12  6083  relimasn  6089  elimasni  6095  inisegn0  6102  predprc  6341  dffv3  6879  suppco  8203  supp0cosupp0  8205  ecexr  8700  fodomfi  9273  domunfican  9282  efgrelexlema  19820  dprdsn  20109  cnindis  23430  cnhaus  23492  cmpfi  23546  xkouni  23737  xkoccn  23757  mbfima  25770  ismbf2d  25780  limcnlp  26018  mdeg0  26208  pserulm  26563  old0  28010  made0  28034  neg0s  28197  neg1s  28198  zcuts0  28579  spthispth  30051  dfpth2  30056  pthdlem2  30095  0pth  30454  1pthdlem2  30465  eupth2lemb  30566  disjpreima  32907  imadifxp  32924  2ndimaxp  32969  mptiffisupp  33016  swrdrndisj  33255  gsumpart  33361  esplyfval2  33933  zarclsint  34240  dstrvprob  34840  opelco3  36245  funpartlem  36412  poimirlem1  38250  poimirlem2  38251  poimirlem3  38252  poimirlem4  38253  poimirlem5  38254  poimirlem6  38255  poimirlem7  38256  poimirlem10  38259  poimirlem11  38260  poimirlem12  38261  poimirlem13  38262  poimirlem16  38265  poimirlem17  38266  poimirlem19  38268  poimirlem20  38269  poimirlem22  38271  poimirlem23  38272  poimirlem24  38273  poimirlem25  38274  poimirlem28  38277  poimirlem29  38278  poimirlem31  38280  he0  44490  smfresal  47482  predisj  49566