Theorem ima0 6051

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 5654	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5957	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5904	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5892	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2757	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4299  ran crn 5642   ↾ cres 5643   “ cima 5644

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2702  ax-sep 5254  ax-nul 5264  ax-pr 5390

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-rab 3409  df-v 3452  df-dif 3920  df-un 3922  df-in 3924  df-ss 3934  df-nul 4300  df-if 4492  df-sn 4593  df-pr 4595  df-op 4599  df-br 5111  df-opab 5173  df-xp 5647  df-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  csbima12  6053  relimasn  6059  elimasni  6065  inisegn0  6072  predprc  6314  dffv3  6857  suppco  8188  supp0cosupp0  8190  ecexr  8679  fodomfi  9268  imafiOLD  9272  domunfican  9279  fodomfiOLD  9288  efgrelexlema  19686  dprdsn  19975  cnindis  23186  cnhaus  23248  cmpfi  23302  xkouni  23493  xkoccn  23513  mbfima  25538  ismbf2d  25548  limcnlp  25786  mdeg0  25982  pserulm  26338  old0  27774  made0  27792  negs0s  27939  negs1s  27940  spthispth  29661  dfpth2  29666  pthdlem2  29705  0pth  30061  1pthdlem2  30072  eupth2lemb  30173  disjpreima  32520  imadifxp  32537  2ndimaxp  32577  mptiffisupp  32623  swrdrndisj  32886  gsumpart  33004  zarclsint  33869  dstrvprob  34470  opelco3  35769  funpartlem  35937  poimirlem1  37622  poimirlem2  37623  poimirlem3  37624  poimirlem4  37625  poimirlem5  37626  poimirlem6  37627  poimirlem7  37628  poimirlem10  37631  poimirlem11  37632  poimirlem12  37633  poimirlem13  37634  poimirlem16  37637  poimirlem17  37638  poimirlem19  37640  poimirlem20  37641  poimirlem22  37643  poimirlem23  37644  poimirlem24  37645  poimirlem25  37646  poimirlem28  37649  poimirlem29  37650  poimirlem31  37652  he0  43780  smfresal  46793  predisj  48803