Theorem ima0 5696

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 5323	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5602	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5553	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5579	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2823	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1653  ∅c0 4113  ran crn 5311   ↾ cres 5312   “ cima 5313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775  ax-sep 4973  ax-nul 4981  ax-pr 5095

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-mo 2590  df-eu 2607  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-br 4842  df-opab 4904  df-xp 5316  df-cnv 5318  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323

This theorem is referenced by:  csbima12  5698  relimasn  5703  elimasni  5707  inisegn0  5712  dffv3  6405  supp0cosupp0  7570  imacosupp  7571  ecexr  7985  domunfican  8473  fodomfi  8479  efgrelexlema  18474  dprdsn  18748  cnindis  21422  cnhaus  21484  cmpfi  21537  xkouni  21728  xkoccn  21748  mbfima  23735  ismbf2d  23745  limcnlp  23980  mdeg0  24168  pserulm  24514  spthispth  26972  pthdlem2  27014  0pth  27461  1pthdlem2  27472  eupth2lemb  27574  disjpreima  29906  imadifxp  29923  dstrvprob  31042  opelco3  32182  funpartlem  32554  poimirlem1  33891  poimirlem2  33892  poimirlem3  33893  poimirlem4  33894  poimirlem5  33895  poimirlem6  33896  poimirlem7  33897  poimirlem10  33900  poimirlem11  33901  poimirlem12  33902  poimirlem13  33903  poimirlem16  33906  poimirlem17  33907  poimirlem19  33909  poimirlem20  33910  poimirlem22  33912  poimirlem23  33913  poimirlem24  33914  poimirlem25  33915  poimirlem28  33918  poimirlem29  33919  poimirlem31  33921  he0  38848  smfresal  41729