Theorem imaeq1 6048

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

This proof depends on syntax axioms:   → wi 4   = wceq 1569  ran crn 5651   ↾ cres 5652   “ cima 5653

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1572  df-fal 1582  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-rab 3413  df-v 3452  df-ss 3897  df-dif 4046  df-in 4090  df-un 4150  df-nul 4278  df-if 4482  df-sn 4585  df-pr 4587  df-op 4835  df-br 5103  df-opab 5167  df-cnv 5658  df-dm 5660  df-rn 5661  df-res 5662  df-ima 5663

This theorem is used by:  imaeq1i  6050  imaeq1d  6052  suppval  8183  naddcllem  8690  eceq2  8764  marypha1lem  9430  marypha1  9431  ackbij2lem2  10322  ackbij2lem3  10323  hfom  10326  limsupval  15648  isacs1i  17838  mreacs  17839  islindf  22125  iscnp  23562  xkoccn  23945  xkohaus  23979  xkoco1cn  23983  xkoco2cn  23984  xkococnlem  23985  xkococn  23986  xkoinjcn  24013  fmval  24269  fmf  24271  utoptop  24560  restutop  24563  restutopopn  24564  ustuqtoplem  24565  ustuqtop1  24567  ustuqtop2  24568  ustuqtop4  24570  ustuqtop5  24571  utopsnneiplem  24573  utopsnnei  24575  neipcfilu  24621  psmetutop  24893  cfilfval  25592  elply2  26521  coeeu  26551  coelem  26552  coeeq  26553  dmarea  27292  negsval  28418  mclsax  36422  tailfval  37254  bj-cleq  37969  bj-funun  38280  poimirlem15  38660  poimirlem24  38669  brtrclfv2  44834  liminfval  46876  ushggricedg  49132  uhgrimisgrgric  49136