Theorem imaeq1 6051

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 5966	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5922	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5668	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5668	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2820	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5656   ↾ cres 5657   “ cima 5658

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 2147  ax-9 2155  ax-ext 2732

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 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5663  df-dm 5665  df-rn 5666  df-res 5667  df-ima 5668

This theorem is used by:  imaeq1i  6053  imaeq1d  6055  suppval  8160  naddcllem  8664  eceq2  8738  marypha1lem  9403  marypha1  9404  ackbij2lem2  10241  ackbij2lem3  10242  r1om  10245  limsupval  15561  isacs1i  17745  mreacs  17746  islindf  22025  iscnp  23462  xkoccn  23845  xkohaus  23879  xkoco1cn  23883  xkoco2cn  23884  xkococnlem  23885  xkococn  23886  xkoinjcn  23913  fmval  24169  fmf  24171  utoptop  24460  restutop  24463  restutopopn  24464  ustuqtoplem  24465  ustuqtop1  24467  ustuqtop2  24468  ustuqtop4  24470  ustuqtop5  24471  utopsnneiplem  24473  utopsnnei  24475  neipcfilu  24521  psmetutop  24793  cfilfval  25492  elply2  26421  coeeu  26451  coelem  26452  coeeq  26453  dmarea  27194  negsval  28290  mclsax  36148  tailfval  36991  bj-cleq  37706  bj-funun  38004  poimirlem15  38384  poimirlem24  38393  brtrclfv2  44567  liminfval  46587  ushggricedg  48843  uhgrimisgrgric  48847