Theorem ima0 6066

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 5679	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5975	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5926	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5915	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2756	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1533  ∅c0 4314  ran crn 5667   ↾ cres 5668   “ cima 5669

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1905  ax-6 1963  ax-7 2003  ax-8 2100  ax-9 2108  ax-10 2129  ax-11 2146  ax-12 2163  ax-ext 2695  ax-sep 5289  ax-nul 5296  ax-pr 5417

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 845  df-3an 1086  df-tru 1536  df-fal 1546  df-ex 1774  df-nf 1778  df-sb 2060  df-clab 2702  df-cleq 2716  df-clel 2802  df-rab 3425  df-v 3468  df-dif 3943  df-un 3945  df-in 3947  df-ss 3957  df-nul 4315  df-if 4521  df-sn 4621  df-pr 4623  df-op 4627  df-br 5139  df-opab 5201  df-xp 5672  df-cnv 5674  df-dm 5676  df-rn 5677  df-res 5678  df-ima 5679

This theorem is referenced by:  csbima12  6068  relimasn  6073  elimasni  6080  inisegn0  6087  predprc  6329  dffv3  6877  suppco  8186  supp0cosupp0  8188  ecexr  8704  imafi  9171  domunfican  9316  fodomfi  9321  efgrelexlema  19659  dprdsn  19948  cnindis  23118  cnhaus  23180  cmpfi  23234  xkouni  23425  xkoccn  23445  mbfima  25481  ismbf2d  25491  limcnlp  25729  mdeg0  25928  pserulm  26275  old0  27702  made0  27716  negs0s  27855  spthispth  29452  pthdlem2  29494  0pth  29847  1pthdlem2  29858  eupth2lemb  29959  disjpreima  32284  imadifxp  32301  2ndimaxp  32341  mptiffisupp  32384  swrdrndisj  32588  gsumpart  32675  zarclsint  33341  dstrvprob  33959  opelco3  35241  funpartlem  35409  poimirlem1  36979  poimirlem2  36980  poimirlem3  36981  poimirlem4  36982  poimirlem5  36983  poimirlem6  36984  poimirlem7  36985  poimirlem10  36988  poimirlem11  36989  poimirlem12  36990  poimirlem13  36991  poimirlem16  36994  poimirlem17  36995  poimirlem19  36997  poimirlem20  36998  poimirlem22  37000  poimirlem23  37001  poimirlem24  37002  poimirlem25  37003  poimirlem28  37006  poimirlem29  37007  poimirlem31  37009  he0  43024  smfresal  45989  predisj  47683