Theorem ima0 6031

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 5633	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5937	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5881	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5870	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2762	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1542  ∅c0 4263  ran crn 5621   ↾ cres 5622   “ cima 5623

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 2707  ax-sep 5220  ax-pr 5364

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 2714  df-cleq 2727  df-clel 2810  df-rab 3388  df-v 3429  df-dif 3888  df-un 3890  df-in 3892  df-ss 3902  df-nul 4264  df-if 4457  df-sn 4558  df-pr 4560  df-op 4564  df-br 5075  df-opab 5137  df-xp 5626  df-cnv 5628  df-dm 5630  df-rn 5631  df-res 5632  df-ima 5633

This theorem is referenced by:  csbima12  6033  relimasn  6039  elimasni  6045  inisegn0  6052  predprc  6291  dffv3  6825  suppco  8145  supp0cosupp0  8147  ecexr  8637  fodomfi  9211  imafiOLD  9215  domunfican  9221  fodomfiOLD  9229  efgrelexlema  19713  dprdsn  20002  cnindis  23245  cnhaus  23307  cmpfi  23361  xkouni  23552  xkoccn  23572  mbfima  25585  ismbf2d  25595  limcnlp  25833  mdeg0  26023  pserulm  26375  old0  27819  made0  27843  neg0s  28006  neg1s  28007  zcuts0  28388  spthispth  29780  dfpth2  29785  pthdlem2  29824  0pth  30183  1pthdlem2  30194  eupth2lemb  30295  disjpreima  32642  imadifxp  32659  2ndimaxp  32707  mptiffisupp  32754  swrdrndisj  33005  gsumpart  33112  esplyfval2  33697  zarclsint  34004  dstrvprob  34604  opelco3  35945  funpartlem  36112  poimirlem1  37930  poimirlem2  37931  poimirlem3  37932  poimirlem4  37933  poimirlem5  37934  poimirlem6  37935  poimirlem7  37936  poimirlem10  37939  poimirlem11  37940  poimirlem12  37941  poimirlem13  37942  poimirlem16  37945  poimirlem17  37946  poimirlem19  37948  poimirlem20  37949  poimirlem22  37951  poimirlem23  37952  poimirlem24  37953  poimirlem25  37954  poimirlem28  37957  poimirlem29  37958  poimirlem31  37960  he0  44199  smfresal  47204  predisj  49274