Theorem imaeq1 5676

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 5592	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5554	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5323	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5323	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2856	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1653  ran crn 5311   ↾ cres 5312   “ cima 5313

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-13 2354  ax-ext 2775

This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-3an 1110  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-rab 3096  df-v 3385  df-dif 3770  df-un 3772  df-in 3774  df-ss 3781  df-nul 4114  df-if 4276  df-sn 4367  df-pr 4369  df-op 4373  df-br 4842  df-opab 4904  df-cnv 5318  df-dm 5320  df-rn 5321  df-res 5322  df-ima 5323

This theorem is referenced by:  imaeq1i  5678  imaeq1d  5680  suppval  7532  eceq2  8020  marypha1lem  8579  marypha1  8580  ackbij2lem2  9348  ackbij2lem3  9349  r1om  9352  limsupval  14543  isacs1i  16629  mreacs  16630  islindf  20473  iscnp  21367  xkoccn  21748  xkohaus  21782  xkoco1cn  21786  xkoco2cn  21787  xkococnlem  21788  xkococn  21789  xkoinjcn  21816  fmval  22072  fmf  22074  utoptop  22363  restutop  22366  restutopopn  22367  ustuqtoplem  22368  ustuqtop1  22370  ustuqtop2  22371  ustuqtop4  22373  ustuqtop5  22374  utopsnneiplem  22376  utopsnnei  22378  neipcfilu  22425  psmetutop  22697  cfilfval  23387  elply2  24290  coeeu  24319  coelem  24320  coeeq  24321  dmarea  25033  mclsax  31975  tailfval  32871  bj-cleq  33433  poimirlem15  33905  poimirlem24  33914  brtrclfv2  38790  liminfval  40723  isomgreqve  42483  isomgrsym  42494  isomgrtr  42497  ushrisomgr  42499