Theorem imaeq1 6056

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 5971	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5927	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5673	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5673	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2822	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ran crn 5661   ↾ cres 5662   “ cima 5663

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1824  ax-4 1838  ax-5 1939  ax-6 1996  ax-7 2037  ax-8 2144  ax-9 2152  ax-ext 2734

This proof depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1104  df-tru 1572  df-fal 1582  df-ex 1809  df-sb 2096  df-clab 2741  df-cleq 2754  df-clel 2837  df-rab 3416  df-v 3456  df-dif 3907  df-un 3909  df-in 3911  df-ss 3921  df-nul 4286  df-if 4487  df-sn 4589  df-pr 4591  df-op 4595  df-br 5109  df-opab 5173  df-cnv 5668  df-dm 5670  df-rn 5671  df-res 5672  df-ima 5673

This theorem is used by:  imaeq1i  6058  imaeq1d  6060  suppval  8156  naddcllem  8660  eceq2  8734  marypha1lem  9391  marypha1  9392  ackbij2lem2  10229  ackbij2lem3  10230  r1om  10233  limsupval  15532  isacs1i  17719  mreacs  17720  islindf  21973  iscnp  23405  xkoccn  23787  xkohaus  23821  xkoco1cn  23825  xkoco2cn  23826  xkococnlem  23827  xkococn  23828  xkoinjcn  23855  fmval  24111  fmf  24113  utoptop  24402  restutop  24405  restutopopn  24406  ustuqtoplem  24407  ustuqtop1  24409  ustuqtop2  24410  ustuqtop4  24412  ustuqtop5  24413  utopsnneiplem  24415  utopsnnei  24417  neipcfilu  24463  psmetutop  24735  cfilfval  25434  elply2  26364  coeeu  26393  coelem  26394  coeeq  26395  dmarea  27133  negsval  28229  mclsax  36069  tailfval  36911  bj-cleq  37626  bj-funun  37924  poimirlem15  38314  poimirlem24  38323  brtrclfv2  44481  liminfval  46501  ushggricedg  48720  uhgrimisgrgric  48724