Theorem ima0 6074

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 5663	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5973	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5918	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5907	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2787	1 ⊢ (𝐴 “ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1569  ∅c0 4278  ran crn 5651   ↾ cres 5652   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732  ax-sep 5248  ax-pr 5390

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3896  df-dif 4047  df-in 4091  df-un 4151  df-nul 4279  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-xp 5656  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  csbima12  6075  relimasn  6082  elimasni  6088  inisegn0  6095  predprc  6341  dffv3  6881  suppco  8226  supp0cosupp0  8228  ecexr  8725  fodomfi  9307  domunfican  9316  efgrelexlema  19968  dprdsn  20257  cnindis  23615  cnhaus  23677  cmpfi  23731  xkouni  23923  xkoccn  23943  mbfima  25956  ismbf2d  25966  limcnlp  26203  mdeg0  26393  pserulm  26754  old0  28230  made0  28254  neg0s  28417  neg1s  28418  zcuts0  28799  spthispth  30314  dfpth2  30319  pthdlem2  30359  0pth  30721  1pthdlem2  30732  eupth2lemb  30843  disjpreima  33225  imadifxp  33242  2ndimaxp  33287  mptiffisupp  33333  swrdrndisj  33564  gsumpart  33670  esplyfval2  34243  zarclsint  34550  dstrvprob  35150  opelco3  36631  funpartlem  36798  poimirlem1  38632  poimirlem2  38633  poimirlem3  38634  poimirlem4  38635  poimirlem5  38636  poimirlem6  38637  poimirlem7  38638  poimirlem10  38641  poimirlem11  38642  poimirlem12  38643  poimirlem13  38644  poimirlem16  38647  poimirlem17  38648  poimirlem19  38650  poimirlem20  38651  poimirlem22  38653  poimirlem23  38654  poimirlem24  38655  poimirlem25  38656  poimirlem28  38659  poimirlem29  38660  poimirlem31  38662  he0  44877  smfresal  47891  predisj  50014