Theorem ima0 5632

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 5276	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5550	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5502	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5527	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2800	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1634  ∅c0 4073  ran crn 5264   ↾ cres 5265   “ cima 5266

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1873  ax-4 1888  ax-5 1994  ax-6 2060  ax-7 2096  ax-9 2157  ax-10 2177  ax-11 2193  ax-12 2206  ax-13 2411  ax-ext 2754  ax-sep 4928  ax-nul 4936  ax-pr 5048

This theorem depends on definitions:  df-bi 198  df-an 384  df-or 864  df-3an 1100  df-tru 1637  df-ex 1856  df-nf 1861  df-sb 2053  df-eu 2625  df-mo 2626  df-clab 2761  df-cleq 2767  df-clel 2770  df-nfc 2905  df-rab 3073  df-v 3357  df-dif 3732  df-un 3734  df-in 3736  df-ss 3743  df-nul 4074  df-if 4236  df-sn 4327  df-pr 4329  df-op 4333  df-br 4798  df-opab 4860  df-xp 5269  df-cnv 5271  df-dm 5273  df-rn 5274  df-res 5275  df-ima 5276

This theorem is referenced by:  csbima12  5634  relimasn  5639  elimasni  5643  inisegn0  5648  dffv3  6344  supp0cosupp0  7507  imacosupp  7508  ecexr  7922  domunfican  8410  fodomfi  8416  efgrelexlema  18389  dprdsn  18663  cnindis  21337  cnhaus  21399  cmpfi  21452  xkouni  21643  xkoccn  21663  mbfima  23638  ismbf2d  23648  limcnlp  23883  mdeg0  24071  pserulm  24417  spthispth  26878  pthdlem2  26920  0pth  27326  1pthdlem2  27337  eupth2lemb  27438  disjpreima  29752  imadifxp  29769  dstrvprob  30890  opelco3  32031  funpartlem  32403  poimirlem1  33760  poimirlem2  33761  poimirlem3  33762  poimirlem4  33763  poimirlem5  33764  poimirlem6  33765  poimirlem7  33766  poimirlem10  33769  poimirlem11  33770  poimirlem12  33771  poimirlem13  33772  poimirlem16  33775  poimirlem17  33776  poimirlem19  33778  poimirlem20  33779  poimirlem22  33781  poimirlem23  33782  poimirlem24  33783  poimirlem25  33784  poimirlem28  33787  poimirlem29  33788  poimirlem31  33790  he0  38618  smfresal  41521