Theorem imaeq1 6059

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 5930	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5676	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5676	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2825	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5664   ↾ cres 5665   “ cima 5666

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-rab 3419  df-v 3459  df-dif 3909  df-un 3911  df-in 3913  df-ss 3923  df-nul 4287  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5112  df-opab 5176  df-cnv 5671  df-dm 5673  df-rn 5674  df-res 5675  df-ima 5676

This theorem is used by:  imaeq1i  6061  imaeq1d  6063  suppval  8164  naddcllem  8668  eceq2  8742  marypha1lem  9400  marypha1  9401  ackbij2lem2  10238  ackbij2lem3  10239  r1om  10242  limsupval  15549  isacs1i  17735  mreacs  17736  islindf  22012  iscnp  23444  xkoccn  23827  xkohaus  23861  xkoco1cn  23865  xkoco2cn  23866  xkococnlem  23867  xkococn  23868  xkoinjcn  23895  fmval  24151  fmf  24153  utoptop  24442  restutop  24445  restutopopn  24446  ustuqtoplem  24447  ustuqtop1  24449  ustuqtop2  24450  ustuqtop4  24452  ustuqtop5  24453  utopsnneiplem  24455  utopsnnei  24457  neipcfilu  24503  psmetutop  24775  cfilfval  25474  elply2  26404  coeeu  26433  coelem  26434  coeeq  26435  dmarea  27173  negsval  28269  mclsax  36098  tailfval  36940  bj-cleq  37655  bj-funun  37953  poimirlem15  38343  poimirlem24  38352  brtrclfv2  44511  liminfval  46531  ushggricedg  48750  uhgrimisgrgric  48754