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-dif 3899  df-un 3901  df-in 3903  df-ss 3914  df-nul 4279  df-if 4482  df-sn 4584  df-pr 4586  df-op 4590  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  8223  supp0cosupp0  8225  ecexr  8722  fodomfi  9304  domunfican  9313  efgrelexlema  19963  dprdsn  20252  cnindis  23610  cnhaus  23672  cmpfi  23726  xkouni  23918  xkoccn  23938  mbfima  25951  ismbf2d  25961  limcnlp  26198  mdeg0  26388  pserulm  26749  old0  28225  made0  28249  neg0s  28412  neg1s  28413  zcuts0  28794  spthispth  30309  dfpth2  30314  pthdlem2  30354  0pth  30716  1pthdlem2  30727  eupth2lemb  30838  disjpreima  33178  imadifxp  33195  2ndimaxp  33240  mptiffisupp  33286  swrdrndisj  33518  gsumpart  33624  esplyfval2  34197  zarclsint  34504  dstrvprob  35104  opelco3  36539  funpartlem  36706  poimirlem1  38540  poimirlem2  38541  poimirlem3  38542  poimirlem4  38543  poimirlem5  38544  poimirlem6  38545  poimirlem7  38546  poimirlem10  38549  poimirlem11  38550  poimirlem12  38551  poimirlem13  38552  poimirlem16  38555  poimirlem17  38556  poimirlem19  38558  poimirlem20  38559  poimirlem22  38561  poimirlem23  38562  poimirlem24  38563  poimirlem25  38564  poimirlem28  38567  poimirlem29  38568  poimirlem31  38570  he0  44784  smfresal  47798  predisj  49921