Theorem ima0 6071

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 5664	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5974	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5919	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5908	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2788	1 ⊢ (𝐴 “ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4279  ran crn 5652   ↾ cres 5653   “ cima 5654

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733  ax-sep 5249  ax-pr 5391

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-xp 5657  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  csbima12  6073  relimasn  6079  elimasni  6085  inisegn0  6092  predprc  6334  dffv3  6873  suppco  8207  supp0cosupp0  8209  ecexr  8706  fodomfi  9288  domunfican  9297  efgrelexlema  19943  dprdsn  20232  cnindis  23590  cnhaus  23652  cmpfi  23706  xkouni  23898  xkoccn  23918  mbfima  25931  ismbf2d  25941  limcnlp  26178  mdeg0  26368  pserulm  26731  old0  28207  made0  28231  neg0s  28394  neg1s  28395  zcuts0  28776  spthispth  30291  dfpth2  30296  pthdlem2  30336  0pth  30698  1pthdlem2  30709  eupth2lemb  30820  disjpreima  33160  imadifxp  33177  2ndimaxp  33222  mptiffisupp  33268  swrdrndisj  33500  gsumpart  33606  esplyfval2  34179  zarclsint  34486  dstrvprob  35087  opelco3  36509  funpartlem  36676  poimirlem1  38507  poimirlem2  38508  poimirlem3  38509  poimirlem4  38510  poimirlem5  38511  poimirlem6  38512  poimirlem7  38513  poimirlem10  38516  poimirlem11  38517  poimirlem12  38518  poimirlem13  38519  poimirlem16  38522  poimirlem17  38523  poimirlem19  38525  poimirlem20  38526  poimirlem22  38528  poimirlem23  38529  poimirlem24  38530  poimirlem25  38531  poimirlem28  38534  poimirlem29  38535  poimirlem31  38537  he0  44743  smfresal  47742  predisj  49865