Theorem imaeq1 6040

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 5955	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5910	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5656	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5656	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1559  ran crn 5644   ↾ cres 5645   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  imaeq1i  6042  imaeq1d  6044  suppval  8136  naddcllem  8640  eceq2  8714  marypha1lem  9373  marypha1  9374  ackbij2lem2  10189  ackbij2lem3  10190  r1om  10193  limsupval  15492  isacs1i  17680  mreacs  17681  islindf  21852  iscnp  23285  xkoccn  23667  xkohaus  23701  xkoco1cn  23705  xkoco2cn  23706  xkococnlem  23707  xkococn  23708  xkoinjcn  23735  fmval  23991  fmf  23993  utoptop  24282  restutop  24285  restutopopn  24286  ustuqtoplem  24287  ustuqtop1  24289  ustuqtop2  24290  ustuqtop4  24292  ustuqtop5  24293  utopsnneiplem  24295  utopsnnei  24297  neipcfilu  24343  psmetutop  24615  cfilfval  25314  elply2  26244  coeeu  26273  coelem  26274  coeeq  26275  dmarea  27010  negsval  28106  mclsax  35880  tailfval  36693  bj-cleq  37408  bj-funun  37705  poimirlem15  38095  poimirlem24  38104  brtrclfv2  44264  liminfval  46294  ushggricedg  48510  uhgrimisgrgric  48514