Theorem ima0 6034

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 5651	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5946	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5897	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5886	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2763	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1541  ∅c0 4287  ran crn 5639   ↾ cres 5640   “ cima 5641

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2702  ax-sep 5261  ax-nul 5268  ax-pr 5389

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-nf 1786  df-sb 2068  df-clab 2709  df-cleq 2723  df-clel 2809  df-rab 3406  df-v 3448  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4288  df-if 4492  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5173  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  csbima12  6036  relimasn  6041  elimasni  6048  inisegn0  6055  predprc  6297  dffv3  6843  suppco  8142  supp0cosupp0  8144  ecexr  8660  imafi  9126  domunfican  9271  fodomfi  9276  efgrelexlema  19545  dprdsn  19829  cnindis  22680  cnhaus  22742  cmpfi  22796  xkouni  22987  xkoccn  23007  mbfima  25031  ismbf2d  25041  limcnlp  25279  mdeg0  25472  pserulm  25818  old0  27232  made0  27246  negs0s  27368  spthispth  28737  pthdlem2  28779  0pth  29132  1pthdlem2  29143  eupth2lemb  29244  disjpreima  31569  imadifxp  31586  2ndimaxp  31630  mptiffisupp  31675  swrdrndisj  31881  gsumpart  31967  zarclsint  32542  dstrvprob  33160  opelco3  34435  funpartlem  34603  poimirlem1  36152  poimirlem2  36153  poimirlem3  36154  poimirlem4  36155  poimirlem5  36156  poimirlem6  36157  poimirlem7  36158  poimirlem10  36161  poimirlem11  36162  poimirlem12  36163  poimirlem13  36164  poimirlem16  36167  poimirlem17  36168  poimirlem19  36170  poimirlem20  36171  poimirlem22  36173  poimirlem23  36174  poimirlem24  36175  poimirlem25  36176  poimirlem28  36179  poimirlem29  36180  poimirlem31  36182  he0  42178  smfresal  45149  predisj  47015