Theorem ima0 6087

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 5668	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5985	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5926	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5915	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2790	1 ⊢ (𝐴 “ ∅) = ∅

This proof depends on syntax axioms:   = wceq 1570  ∅c0 4281  ran crn 5656   ↾ cres 5657   “ cima 5658

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735  ax-sep 5252  ax-pr 5395

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 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4839  df-br 5107  df-opab 5171  df-xp 5661  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  csbima12  6088  relimasn  6095  elimasni  6101  inisegn0  6108  predprc  6359  dffv3  6904  suppco  8251  supp0cosupp0  8253  ecexr  8750  fodomfi  9332  domunfican  9341  efgrelexlema  19993  dprdsn  20282  cnindis  23640  cnhaus  23702  cmpfi  23756  xkouni  23948  xkoccn  23968  mbfima  25981  ismbf2d  25991  limcnlp  26228  mdeg0  26418  pserulm  26779  old0  28255  made0  28279  neg0s  28442  neg1s  28443  zcuts0  28824  spthispth  30339  dfpth2  30344  pthdlem2  30384  0pth  30746  1pthdlem2  30757  eupth2lemb  30868  disjpreima  33250  imadifxp  33267  2ndimaxp  33312  mptiffisupp  33357  swrdrndisj  33588  gsumpart  33694  esplyfval2  34267  zarclsint  34574  dstrvprob  35174  opelco3  36717  funpartlem  36884  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem4  38734  poimirlem5  38735  poimirlem6  38736  poimirlem7  38737  poimirlem10  38740  poimirlem11  38741  poimirlem12  38742  poimirlem13  38743  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem22  38752  poimirlem23  38753  poimirlem24  38754  poimirlem25  38755  poimirlem28  38758  poimirlem29  38759  poimirlem31  38761  he0  44976  smfresal  48003  predisj  50126