Theorem ima0 6077

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 5690	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5986	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5937	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5926	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2765	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1542  ∅c0 4323  ran crn 5678   ↾ cres 5679   “ cima 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704  ax-sep 5300  ax-nul 5307  ax-pr 5428

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690

This theorem is referenced by:  csbima12  6079  relimasn  6084  elimasni  6091  inisegn0  6098  predprc  6340  dffv3  6888  suppco  8191  supp0cosupp0  8193  ecexr  8708  imafi  9175  domunfican  9320  fodomfi  9325  efgrelexlema  19617  dprdsn  19906  cnindis  22796  cnhaus  22858  cmpfi  22912  xkouni  23103  xkoccn  23123  mbfima  25147  ismbf2d  25157  limcnlp  25395  mdeg0  25588  pserulm  25934  old0  27354  made0  27368  negs0s  27501  spthispth  28983  pthdlem2  29025  0pth  29378  1pthdlem2  29389  eupth2lemb  29490  disjpreima  31815  imadifxp  31832  2ndimaxp  31872  mptiffisupp  31915  swrdrndisj  32121  gsumpart  32207  zarclsint  32852  dstrvprob  33470  opelco3  34746  funpartlem  34914  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem28  36516  poimirlem29  36517  poimirlem31  36519  he0  42535  smfresal  45504  predisj  47495