Theorem imaeq1 6057

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 5972	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5928	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5674	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5674	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1570  ran crn 5662   ↾ cres 5663   “ cima 5664

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-rab 3417  df-v 3457  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4488  df-sn 4590  df-pr 4592  df-op 4596  df-br 5110  df-opab 5174  df-cnv 5669  df-dm 5671  df-rn 5672  df-res 5673  df-ima 5674

This theorem is referenced by:  imaeq1i  6059  imaeq1d  6061  suppval  8154  naddcllem  8658  eceq2  8732  marypha1lem  9389  marypha1  9390  ackbij2lem2  10218  ackbij2lem3  10219  r1om  10222  limsupval  15521  isacs1i  17708  mreacs  17709  islindf  21962  iscnp  23394  xkoccn  23776  xkohaus  23810  xkoco1cn  23814  xkoco2cn  23815  xkococnlem  23816  xkococn  23817  xkoinjcn  23844  fmval  24100  fmf  24102  utoptop  24391  restutop  24394  restutopopn  24395  ustuqtoplem  24396  ustuqtop1  24398  ustuqtop2  24399  ustuqtop4  24401  ustuqtop5  24402  utopsnneiplem  24404  utopsnnei  24406  neipcfilu  24452  psmetutop  24724  cfilfval  25423  elply2  26353  coeeu  26382  coelem  26383  coeeq  26384  dmarea  27122  negsval  28218  mclsax  36061  tailfval  36883  bj-cleq  37598  bj-funun  37896  poimirlem15  38286  poimirlem24  38295  brtrclfv2  44453  liminfval  46473  ushggricedg  48692  uhgrimisgrgric  48696