Theorem imaeq1 6011

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 5929	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5885	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5634	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5634	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2793	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1541  ran crn 5622   ↾ cres 5623   “ cima 5624

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 2705

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 2712  df-cleq 2725  df-clel 2808  df-rab 3398  df-v 3440  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4285  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  imaeq1i  6013  imaeq1d  6015  suppval  8101  naddcllem  8600  eceq2  8672  marypha1lem  9327  marypha1  9328  ackbij2lem2  10140  ackbij2lem3  10141  r1om  10144  limsupval  15391  isacs1i  17573  mreacs  17574  islindf  21759  iscnp  23162  xkoccn  23544  xkohaus  23578  xkoco1cn  23582  xkoco2cn  23583  xkococnlem  23584  xkococn  23585  xkoinjcn  23612  fmval  23868  fmf  23870  utoptop  24159  restutop  24162  restutopopn  24163  ustuqtoplem  24164  ustuqtop1  24166  ustuqtop2  24167  ustuqtop4  24169  ustuqtop5  24170  utopsnneiplem  24172  utopsnnei  24174  neipcfilu  24220  psmetutop  24492  cfilfval  25201  elply2  26138  coeeu  26167  coelem  26168  coeeq  26169  dmarea  26904  negsval  27977  mclsax  35624  tailfval  36427  bj-cleq  37017  bj-funun  37307  poimirlem15  37685  poimirlem24  37694  brtrclfv2  43834  liminfval  45871  ushggricedg  48041  uhgrimisgrgric  48045