Theorem imaeq1 6073

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 5991	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5949	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5698	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5698	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2802	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5686   ↾ cres 5687   “ cima 5688

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-rab 3437  df-v 3482  df-dif 3954  df-un 3956  df-in 3958  df-ss 3968  df-nul 4334  df-if 4526  df-sn 4627  df-pr 4629  df-op 4633  df-br 5144  df-opab 5206  df-cnv 5693  df-dm 5695  df-rn 5696  df-res 5697  df-ima 5698

This theorem is referenced by:  imaeq1i  6075  imaeq1d  6077  suppval  8187  naddcllem  8714  eceq2  8786  marypha1lem  9473  marypha1  9474  ackbij2lem2  10279  ackbij2lem3  10280  r1om  10283  limsupval  15510  isacs1i  17700  mreacs  17701  islindf  21832  iscnp  23245  xkoccn  23627  xkohaus  23661  xkoco1cn  23665  xkoco2cn  23666  xkococnlem  23667  xkococn  23668  xkoinjcn  23695  fmval  23951  fmf  23953  utoptop  24243  restutop  24246  restutopopn  24247  ustuqtoplem  24248  ustuqtop1  24250  ustuqtop2  24251  ustuqtop4  24253  ustuqtop5  24254  utopsnneiplem  24256  utopsnnei  24258  neipcfilu  24305  psmetutop  24580  cfilfval  25298  elply2  26235  coeeu  26264  coelem  26265  coeeq  26266  dmarea  27000  negsval  28057  mclsax  35574  tailfval  36373  bj-cleq  36963  bj-funun  37253  poimirlem15  37642  poimirlem24  37651  brtrclfv2  43740  liminfval  45774  ushggricedg  47896  uhgrimisgrgric  47899