Theorem imaeq1 6075

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 5994	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5952	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5702	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5702	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2800	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1537  ran crn 5690   ↾ cres 5691   “ cima 5692

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1792  ax-4 1806  ax-5 1908  ax-6 1965  ax-7 2005  ax-8 2108  ax-9 2116  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1540  df-fal 1550  df-ex 1777  df-sb 2063  df-clab 2713  df-cleq 2727  df-clel 2814  df-rab 3434  df-v 3480  df-dif 3966  df-un 3968  df-in 3970  df-ss 3980  df-nul 4340  df-if 4532  df-sn 4632  df-pr 4634  df-op 4638  df-br 5149  df-opab 5211  df-cnv 5697  df-dm 5699  df-rn 5700  df-res 5701  df-ima 5702

This theorem is referenced by:  imaeq1i  6077  imaeq1d  6079  suppval  8186  naddcllem  8713  eceq2  8785  marypha1lem  9471  marypha1  9472  ackbij2lem2  10277  ackbij2lem3  10278  r1om  10281  limsupval  15507  isacs1i  17702  mreacs  17703  islindf  21850  iscnp  23261  xkoccn  23643  xkohaus  23677  xkoco1cn  23681  xkoco2cn  23682  xkococnlem  23683  xkococn  23684  xkoinjcn  23711  fmval  23967  fmf  23969  utoptop  24259  restutop  24262  restutopopn  24263  ustuqtoplem  24264  ustuqtop1  24266  ustuqtop2  24267  ustuqtop4  24269  ustuqtop5  24270  utopsnneiplem  24272  utopsnnei  24274  neipcfilu  24321  psmetutop  24596  cfilfval  25312  elply2  26250  coeeu  26279  coelem  26280  coeeq  26281  dmarea  27015  negsval  28072  mclsax  35554  tailfval  36355  bj-cleq  36945  bj-funun  37235  poimirlem15  37622  poimirlem24  37631  brtrclfv2  43717  liminfval  45715  ushggricedg  47834  uhgrimisgrgric  47837