Theorem ima0 6032

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 5636	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5938	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5883	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5872	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2756	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1540  ∅c0 4286  ran crn 5624   ↾ cres 5625   “ cima 5626

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 2701  ax-sep 5238  ax-nul 5248  ax-pr 5374

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 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  csbima12  6034  relimasn  6040  elimasni  6046  inisegn0  6053  predprc  6290  dffv3  6822  suppco  8146  supp0cosupp0  8148  ecexr  8637  fodomfi  9219  imafiOLD  9223  domunfican  9230  fodomfiOLD  9239  efgrelexlema  19646  dprdsn  19935  cnindis  23195  cnhaus  23257  cmpfi  23311  xkouni  23502  xkoccn  23522  mbfima  25547  ismbf2d  25557  limcnlp  25795  mdeg0  25991  pserulm  26347  old0  27787  made0  27805  negs0s  27955  negs1s  27956  spthispth  29687  dfpth2  29692  pthdlem2  29731  0pth  30087  1pthdlem2  30098  eupth2lemb  30199  disjpreima  32546  imadifxp  32563  2ndimaxp  32603  mptiffisupp  32649  swrdrndisj  32912  gsumpart  33023  zarclsint  33838  dstrvprob  34439  opelco3  35747  funpartlem  35915  poimirlem1  37600  poimirlem2  37601  poimirlem3  37602  poimirlem4  37603  poimirlem5  37604  poimirlem6  37605  poimirlem7  37606  poimirlem10  37609  poimirlem11  37610  poimirlem12  37611  poimirlem13  37612  poimirlem16  37615  poimirlem17  37616  poimirlem19  37618  poimirlem20  37619  poimirlem22  37621  poimirlem23  37622  poimirlem24  37623  poimirlem25  37624  poimirlem28  37627  poimirlem29  37628  poimirlem31  37630  he0  43757  smfresal  46770  predisj  48796