Theorem imaeq1 6022

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 5940	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5895	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5645	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5645	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2797	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  imaeq1i  6024  imaeq1d  6026  suppval  8114  naddcllem  8614  eceq2  8687  marypha1lem  9348  marypha1  9349  ackbij2lem2  10161  ackbij2lem3  10162  r1om  10165  limsupval  15409  isacs1i  17592  mreacs  17593  islindf  21779  iscnp  23193  xkoccn  23575  xkohaus  23609  xkoco1cn  23613  xkoco2cn  23614  xkococnlem  23615  xkococn  23616  xkoinjcn  23643  fmval  23899  fmf  23901  utoptop  24190  restutop  24193  restutopopn  24194  ustuqtoplem  24195  ustuqtop1  24197  ustuqtop2  24198  ustuqtop4  24200  ustuqtop5  24201  utopsnneiplem  24203  utopsnnei  24205  neipcfilu  24251  psmetutop  24523  cfilfval  25232  elply2  26169  coeeu  26198  coelem  26199  coeeq  26200  dmarea  26935  negsval  28033  mclsax  35785  tailfval  36588  bj-cleq  37210  bj-funun  37507  poimirlem15  37886  poimirlem24  37895  brtrclfv2  44083  liminfval  46117  ushggricedg  48287  uhgrimisgrgric  48291