Theorem ima0 6030

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 5632	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5936	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5881	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5870	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2760	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1541  ∅c0 4282  ran crn 5620   ↾ cres 5621   “ cima 5622

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705  ax-sep 5236  ax-nul 5246  ax-pr 5372

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4475  df-sn 4576  df-pr 4578  df-op 4582  df-br 5094  df-opab 5156  df-xp 5625  df-cnv 5627  df-dm 5629  df-rn 5630  df-res 5631  df-ima 5632

This theorem is referenced by:  csbima12  6032  relimasn  6038  elimasni  6044  inisegn0  6051  predprc  6290  dffv3  6824  suppco  8142  supp0cosupp0  8144  ecexr  8633  fodomfi  9203  imafiOLD  9207  domunfican  9213  fodomfiOLD  9221  efgrelexlema  19663  dprdsn  19952  cnindis  23208  cnhaus  23270  cmpfi  23324  xkouni  23515  xkoccn  23535  mbfima  25559  ismbf2d  25569  limcnlp  25807  mdeg0  26003  pserulm  26359  old0  27801  made0  27819  negs0s  27969  negs1s  27970  spthispth  29704  dfpth2  29709  pthdlem2  29748  0pth  30107  1pthdlem2  30118  eupth2lemb  30219  disjpreima  32566  imadifxp  32583  2ndimaxp  32630  mptiffisupp  32678  swrdrndisj  32945  gsumpart  33044  esplyfval2  33605  zarclsint  33906  dstrvprob  34506  opelco3  35840  funpartlem  36007  poimirlem1  37681  poimirlem2  37682  poimirlem3  37683  poimirlem4  37684  poimirlem5  37685  poimirlem6  37686  poimirlem7  37687  poimirlem10  37690  poimirlem11  37691  poimirlem12  37692  poimirlem13  37693  poimirlem16  37696  poimirlem17  37697  poimirlem19  37699  poimirlem20  37700  poimirlem22  37702  poimirlem23  37703  poimirlem24  37704  poimirlem25  37705  poimirlem28  37708  poimirlem29  37709  poimirlem31  37711  he0  43901  smfresal  46910  predisj  48935