Theorem ima0 6042

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 5644	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5948	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5892	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5881	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2763	1 ⊢ (𝐴 “ ∅) = ∅

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

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 2708  ax-sep 5231  ax-pr 5375

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 2715  df-cleq 2728  df-clel 2811  df-rab 3390  df-v 3431  df-dif 3892  df-un 3894  df-in 3896  df-ss 3906  df-nul 4274  df-if 4467  df-sn 4568  df-pr 4570  df-op 4574  df-br 5086  df-opab 5148  df-xp 5637  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  csbima12  6044  relimasn  6050  elimasni  6056  inisegn0  6063  predprc  6302  dffv3  6836  suppco  8156  supp0cosupp0  8158  ecexr  8648  fodomfi  9222  imafiOLD  9226  domunfican  9232  fodomfiOLD  9240  efgrelexlema  19724  dprdsn  20013  cnindis  23257  cnhaus  23319  cmpfi  23373  xkouni  23564  xkoccn  23584  mbfima  25597  ismbf2d  25607  limcnlp  25845  mdeg0  26035  pserulm  26387  old0  27831  made0  27855  neg0s  28018  neg1s  28019  zcuts0  28400  spthispth  29792  dfpth2  29797  pthdlem2  29836  0pth  30195  1pthdlem2  30206  eupth2lemb  30307  disjpreima  32654  imadifxp  32671  2ndimaxp  32719  mptiffisupp  32766  swrdrndisj  33017  gsumpart  33124  esplyfval2  33709  zarclsint  34016  dstrvprob  34616  opelco3  35957  funpartlem  36124  poimirlem1  37942  poimirlem2  37943  poimirlem3  37944  poimirlem4  37945  poimirlem5  37946  poimirlem6  37947  poimirlem7  37948  poimirlem10  37951  poimirlem11  37952  poimirlem12  37953  poimirlem13  37954  poimirlem16  37957  poimirlem17  37958  poimirlem19  37960  poimirlem20  37961  poimirlem22  37963  poimirlem23  37964  poimirlem24  37965  poimirlem25  37966  poimirlem28  37969  poimirlem29  37970  poimirlem31  37972  he0  44211  smfresal  47216  predisj  49286