Theorem imaeq1 6015

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 5933	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5891	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5644	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5644	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2789	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5632   ↾ cres 5633   “ cima 5634

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 2701

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 2708  df-cleq 2721  df-clel 2803  df-rab 3403  df-v 3446  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4293  df-if 4485  df-sn 4586  df-pr 4588  df-op 4592  df-br 5103  df-opab 5165  df-cnv 5639  df-dm 5641  df-rn 5642  df-res 5643  df-ima 5644

This theorem is referenced by:  imaeq1i  6017  imaeq1d  6019  suppval  8118  naddcllem  8617  eceq2  8689  marypha1lem  9360  marypha1  9361  ackbij2lem2  10168  ackbij2lem3  10169  r1om  10172  limsupval  15416  isacs1i  17594  mreacs  17595  islindf  21697  iscnp  23100  xkoccn  23482  xkohaus  23516  xkoco1cn  23520  xkoco2cn  23521  xkococnlem  23522  xkococn  23523  xkoinjcn  23550  fmval  23806  fmf  23808  utoptop  24098  restutop  24101  restutopopn  24102  ustuqtoplem  24103  ustuqtop1  24105  ustuqtop2  24106  ustuqtop4  24108  ustuqtop5  24109  utopsnneiplem  24111  utopsnnei  24113  neipcfilu  24159  psmetutop  24431  cfilfval  25140  elply2  26077  coeeu  26106  coelem  26107  coeeq  26108  dmarea  26843  negsval  27907  mclsax  35529  tailfval  36333  bj-cleq  36923  bj-funun  37213  poimirlem15  37602  poimirlem24  37611  brtrclfv2  43689  liminfval  45730  ushggricedg  47900  uhgrimisgrgric  47904