Theorem ima0 5722

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 5355	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5633	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5584	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5610	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2853	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1658  ∅c0 4144  ran crn 5343   ↾ cres 5344   “ cima 5345

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1896  ax-4 1910  ax-5 2011  ax-6 2077  ax-7 2114  ax-9 2175  ax-10 2194  ax-11 2209  ax-12 2222  ax-13 2391  ax-ext 2803  ax-sep 5005  ax-nul 5013  ax-pr 5127

This theorem depends on definitions:  df-bi 199  df-an 387  df-or 881  df-3an 1115  df-tru 1662  df-ex 1881  df-nf 1885  df-sb 2070  df-mo 2605  df-eu 2640  df-clab 2812  df-cleq 2818  df-clel 2821  df-nfc 2958  df-rab 3126  df-v 3416  df-dif 3801  df-un 3803  df-in 3805  df-ss 3812  df-nul 4145  df-if 4307  df-sn 4398  df-pr 4400  df-op 4404  df-br 4874  df-opab 4936  df-xp 5348  df-cnv 5350  df-dm 5352  df-rn 5353  df-res 5354  df-ima 5355

This theorem is referenced by:  csbima12  5724  relimasn  5729  elimasni  5733  inisegn0  5738  dffv3  6429  supp0cosupp0  7599  imacosupp  7600  ecexr  8014  domunfican  8502  fodomfi  8508  efgrelexlema  18515  dprdsn  18789  cnindis  21467  cnhaus  21529  cmpfi  21582  xkouni  21773  xkoccn  21793  mbfima  23796  ismbf2d  23806  limcnlp  24041  mdeg0  24229  pserulm  24575  spthispth  27028  pthdlem2  27070  0pth  27501  1pthdlem2  27512  eupth2lemb  27614  disjpreima  29944  imadifxp  29961  dstrvprob  31079  opelco3  32216  funpartlem  32588  poimirlem1  33954  poimirlem2  33955  poimirlem3  33956  poimirlem4  33957  poimirlem5  33958  poimirlem6  33959  poimirlem7  33960  poimirlem10  33963  poimirlem11  33964  poimirlem12  33965  poimirlem13  33966  poimirlem16  33969  poimirlem17  33970  poimirlem19  33972  poimirlem20  33973  poimirlem22  33975  poimirlem23  33976  poimirlem24  33977  poimirlem25  33978  poimirlem28  33981  poimirlem29  33982  poimirlem31  33984  he0  38918  smfresal  41789