Theorem ima0 5516

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 5156	. 2 ⊢ (𝐴 “ ∅) = ran (𝐴 ↾ ∅)
2		res0 5432	. . 3 ⊢ (𝐴 ↾ ∅) = ∅
3	2	rneqi 5384	. 2 ⊢ ran (𝐴 ↾ ∅) = ran ∅
4		rn0 5409	. 2 ⊢ ran ∅ = ∅
5	1, 3, 4	3eqtri 2677	1 ⊢ (𝐴 “ ∅) = ∅

Syntax hints:   = wceq 1523  ∅c0 3948  ran crn 5144   ↾ cres 5145   “ cima 5146

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631  ax-sep 4814  ax-nul 4822  ax-pr 4936

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1056  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-eu 2502  df-mo 2503  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-rab 2950  df-v 3233  df-dif 3610  df-un 3612  df-in 3614  df-ss 3621  df-nul 3949  df-if 4120  df-sn 4211  df-pr 4213  df-op 4217  df-br 4686  df-opab 4746  df-xp 5149  df-cnv 5151  df-dm 5153  df-rn 5154  df-res 5155  df-ima 5156

This theorem is referenced by:  csbima12  5518  relimasn  5523  elimasni  5527  inisegn0  5532  dffv3  6225  supp0cosupp0  7379  imacosupp  7380  ecexr  7792  domunfican  8274  fodomfi  8280  efgrelexlema  18208  dprdsn  18481  cnindis  21144  cnhaus  21206  cmpfi  21259  xkouni  21450  xkoccn  21470  mbfima  23444  ismbf2d  23453  limcnlp  23687  mdeg0  23875  pserulm  24221  spthispth  26678  pthdlem2  26720  0pth  27103  1pthdlem2  27114  eupth2lemb  27215  disjpreima  29523  imadifxp  29540  dstrvprob  30661  opelco3  31802  funpartlem  32174  poimirlem1  33540  poimirlem2  33541  poimirlem3  33542  poimirlem4  33543  poimirlem5  33544  poimirlem6  33545  poimirlem7  33546  poimirlem10  33549  poimirlem11  33550  poimirlem12  33551  poimirlem13  33552  poimirlem16  33555  poimirlem17  33556  poimirlem19  33558  poimirlem20  33559  poimirlem22  33561  poimirlem23  33562  poimirlem24  33563  poimirlem25  33564  poimirlem28  33567  poimirlem29  33568  poimirlem31  33570  he0  38395  smfresal  41316