Theorem imaeq1 6029

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 5947	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5905	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5654	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5654	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2790	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1540  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-ext 2702

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-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-cnv 5649  df-dm 5651  df-rn 5652  df-res 5653  df-ima 5654

This theorem is referenced by:  imaeq1i  6031  imaeq1d  6033  suppval  8144  naddcllem  8643  eceq2  8715  marypha1lem  9391  marypha1  9392  ackbij2lem2  10199  ackbij2lem3  10200  r1om  10203  limsupval  15447  isacs1i  17625  mreacs  17626  islindf  21728  iscnp  23131  xkoccn  23513  xkohaus  23547  xkoco1cn  23551  xkoco2cn  23552  xkococnlem  23553  xkococn  23554  xkoinjcn  23581  fmval  23837  fmf  23839  utoptop  24129  restutop  24132  restutopopn  24133  ustuqtoplem  24134  ustuqtop1  24136  ustuqtop2  24137  ustuqtop4  24139  ustuqtop5  24140  utopsnneiplem  24142  utopsnnei  24144  neipcfilu  24190  psmetutop  24462  cfilfval  25171  elply2  26108  coeeu  26137  coelem  26138  coeeq  26139  dmarea  26874  negsval  27938  mclsax  35563  tailfval  36367  bj-cleq  36957  bj-funun  37247  poimirlem15  37636  poimirlem24  37645  brtrclfv2  43723  liminfval  45764  ushggricedg  47931  uhgrimisgrgric  47935