Theorem imaeq1 6007

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 5925	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5880	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5631	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5631	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2799	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1547  ran crn 5619   ↾ cres 5620   “ cima 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  imaeq1i  6009  imaeq1d  6011  suppval  8102  naddcllem  8602  eceq2  8675  marypha1lem  9336  marypha1  9337  ackbij2lem2  10152  ackbij2lem3  10153  r1om  10156  limsupval  15427  isacs1i  17614  mreacs  17615  islindf  21787  iscnp  23220  xkoccn  23602  xkohaus  23636  xkoco1cn  23640  xkoco2cn  23641  xkococnlem  23642  xkococn  23643  xkoinjcn  23670  fmval  23926  fmf  23928  utoptop  24217  restutop  24220  restutopopn  24221  ustuqtoplem  24222  ustuqtop1  24224  ustuqtop2  24225  ustuqtop4  24227  ustuqtop5  24228  utopsnneiplem  24230  utopsnnei  24232  neipcfilu  24278  psmetutop  24550  cfilfval  25249  elply2  26179  coeeu  26208  coelem  26209  coeeq  26210  dmarea  26939  negsval  28035  mclsax  35797  tailfval  36600  bj-cleq  37315  bj-funun  37612  poimirlem15  38002  poimirlem24  38011  brtrclfv2  44171  liminfval  46202  ushggricedg  48418  uhgrimisgrgric  48422