Theorem ima0 5929

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 5548	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5839	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5790	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5779	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2766	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1542  ∅c0 4221  ran crn 5536   ↾ cres 5537   “ cima 5538

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1975  ax-7 2020  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2162  ax-12 2179  ax-ext 2711  ax-sep 5177  ax-nul 5184  ax-pr 5306

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1787  df-nf 1791  df-sb 2075  df-clab 2718  df-cleq 2731  df-clel 2812  df-rab 3063  df-v 3402  df-dif 3856  df-un 3858  df-in 3860  df-ss 3870  df-nul 4222  df-if 4425  df-sn 4527  df-pr 4529  df-op 4533  df-br 5041  df-opab 5103  df-xp 5541  df-cnv 5543  df-dm 5545  df-rn 5546  df-res 5547  df-ima 5548

This theorem is referenced by:  csbima12  5931  relimasn  5936  elimasni  5940  inisegn0  5945  dffv3  6682  suppco  7913  supp0cosupp0  7915  ecexr  8337  imafi  8785  domunfican  8877  fodomfi  8882  efgrelexlema  19005  dprdsn  19289  cnindis  22055  cnhaus  22117  cmpfi  22171  xkouni  22362  xkoccn  22382  mbfima  24394  ismbf2d  24404  limcnlp  24642  mdeg0  24835  pserulm  25181  spthispth  27679  pthdlem2  27721  0pth  28074  1pthdlem2  28085  eupth2lemb  28186  disjpreima  30509  imadifxp  30526  2ndimaxp  30570  swrdrndisj  30816  gsumpart  30904  zarclsint  31406  dstrvprob  32020  opelco3  33335  old0  33698  made0  33712  negs0s  33779  funpartlem  33899  poimirlem1  35433  poimirlem2  35434  poimirlem3  35435  poimirlem4  35436  poimirlem5  35437  poimirlem6  35438  poimirlem7  35439  poimirlem10  35442  poimirlem11  35443  poimirlem12  35444  poimirlem13  35445  poimirlem16  35448  poimirlem17  35449  poimirlem19  35451  poimirlem20  35452  poimirlem22  35454  poimirlem23  35455  poimirlem24  35456  poimirlem25  35457  poimirlem28  35460  poimirlem29  35461  poimirlem31  35463  he0  40978  smfresal  43901  predisj  45735