Theorem imaeq1 6053

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 5974	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5936	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5689	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5689	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2798	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1542  ran crn 5677   ↾ cres 5678   “ cima 5679

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3951  df-un 3953  df-in 3955  df-ss 3965  df-nul 4323  df-if 4529  df-sn 4629  df-pr 4631  df-op 4635  df-br 5149  df-opab 5211  df-cnv 5684  df-dm 5686  df-rn 5687  df-res 5688  df-ima 5689

This theorem is referenced by:  imaeq1i  6055  imaeq1d  6057  suppval  8145  naddcllem  8672  eceq2  8740  marypha1lem  9425  marypha1  9426  ackbij2lem2  10232  ackbij2lem3  10233  r1om  10236  limsupval  15415  isacs1i  17598  mreacs  17599  islindf  21359  iscnp  22733  xkoccn  23115  xkohaus  23149  xkoco1cn  23153  xkoco2cn  23154  xkococnlem  23155  xkococn  23156  xkoinjcn  23183  fmval  23439  fmf  23441  utoptop  23731  restutop  23734  restutopopn  23735  ustuqtoplem  23736  ustuqtop1  23738  ustuqtop2  23739  ustuqtop4  23741  ustuqtop5  23742  utopsnneiplem  23744  utopsnnei  23746  neipcfilu  23793  psmetutop  24068  cfilfval  24773  elply2  25702  coeeu  25731  coelem  25732  coeeq  25733  dmarea  26452  negsval  27490  mclsax  34549  tailfval  35246  bj-cleq  35832  bj-funun  36122  poimirlem15  36492  poimirlem24  36501  brtrclfv2  42464  liminfval  44462  isomgreqve  46480  isomgrsym  46491  isomgrtr  46494  ushrisomgr  46496