Theorem ima0 6063

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 5658	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5967	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5911	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5900	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2788	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1559  ∅c0 4285  ran crn 5646   ↾ cres 5647   “ cima 5648

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733  ax-sep 5245  ax-pr 5389

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4480  df-sn 4582  df-pr 4584  df-op 4588  df-br 5100  df-opab 5162  df-xp 5651  df-cnv 5653  df-dm 5655  df-rn 5656  df-res 5657  df-ima 5658

This theorem is referenced by:  csbima12  6065  relimasn  6071  elimasni  6077  inisegn0  6084  predprc  6321  dffv3  6859  suppco  8181  supp0cosupp0  8183  ecexr  8678  fodomfi  9252  imafiOLD  9256  domunfican  9262  fodomfiOLD  9270  efgrelexlema  19772  dprdsn  20061  cnindis  23332  cnhaus  23394  cmpfi  23448  xkouni  23639  xkoccn  23659  mbfima  25672  ismbf2d  25682  limcnlp  25920  mdeg0  26110  pserulm  26462  old0  27909  made0  27933  neg0s  28096  neg1s  28097  zcuts0  28478  spthispth  29870  dfpth2  29875  pthdlem2  29914  0pth  30273  1pthdlem2  30284  eupth2lemb  30385  disjpreima  32733  imadifxp  32750  2ndimaxp  32798  mptiffisupp  32845  swrdrndisj  33096  gsumpart  33204  esplyfval2  33823  zarclsint  34130  dstrvprob  34730  opelco3  36089  funpartlem  36256  poimirlem1  38084  poimirlem2  38085  poimirlem3  38086  poimirlem4  38087  poimirlem5  38088  poimirlem6  38089  poimirlem7  38090  poimirlem10  38093  poimirlem11  38094  poimirlem12  38095  poimirlem13  38096  poimirlem16  38099  poimirlem17  38100  poimirlem19  38102  poimirlem20  38103  poimirlem22  38105  poimirlem23  38106  poimirlem24  38107  poimirlem25  38108  poimirlem28  38111  poimirlem29  38112  poimirlem31  38114  he0  44324  smfresal  47326  predisj  49396