Theorem imaeq1 6014

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq1	⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Proof of Theorem imaeq1

Step	Hyp	Ref	Expression
1		reseq1 5932	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5887	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5637	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5637	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2796	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1541  ran crn 5625   ↾ cres 5626   “ cima 5627

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaeq1i  6016  imaeq1d  6018  suppval  8104  naddcllem  8604  eceq2  8676  marypha1lem  9336  marypha1  9337  ackbij2lem2  10149  ackbij2lem3  10150  r1om  10153  limsupval  15397  isacs1i  17580  mreacs  17581  islindf  21767  iscnp  23181  xkoccn  23563  xkohaus  23597  xkoco1cn  23601  xkoco2cn  23602  xkococnlem  23603  xkococn  23604  xkoinjcn  23631  fmval  23887  fmf  23889  utoptop  24178  restutop  24181  restutopopn  24182  ustuqtoplem  24183  ustuqtop1  24185  ustuqtop2  24186  ustuqtop4  24188  ustuqtop5  24189  utopsnneiplem  24191  utopsnnei  24193  neipcfilu  24239  psmetutop  24511  cfilfval  25220  elply2  26157  coeeu  26186  coelem  26187  coeeq  26188  dmarea  26923  negsval  28021  mclsax  35763  tailfval  36566  bj-cleq  37163  bj-funun  37457  poimirlem15  37836  poimirlem24  37845  brtrclfv2  43968  liminfval  46003  ushggricedg  48173  uhgrimisgrgric  48177