Theorem imaeq1 5924

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 5847	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5808	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5568	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5568	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2881	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1537  ran crn 5556   ↾ cres 5557   “ cima 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by:  imaeq1i  5926  imaeq1d  5928  suppval  7832  eceq2  8329  marypha1lem  8897  marypha1  8898  ackbij2lem2  9662  ackbij2lem3  9663  r1om  9666  limsupval  14831  isacs1i  16928  mreacs  16929  islindf  20956  iscnp  21845  xkoccn  22227  xkohaus  22261  xkoco1cn  22265  xkoco2cn  22266  xkococnlem  22267  xkococn  22268  xkoinjcn  22295  fmval  22551  fmf  22553  utoptop  22843  restutop  22846  restutopopn  22847  ustuqtoplem  22848  ustuqtop1  22850  ustuqtop2  22851  ustuqtop4  22853  ustuqtop5  22854  utopsnneiplem  22856  utopsnnei  22858  neipcfilu  22905  psmetutop  23177  cfilfval  23867  elply2  24786  coeeu  24815  coelem  24816  coeeq  24817  dmarea  25535  mclsax  32816  tailfval  33720  bj-cleq  34277  bj-funun  34537  poimirlem15  34922  poimirlem24  34931  brtrclfv2  40121  liminfval  42089  isomgreqve  44039  isomgrsym  44050  isomgrtr  44053  ushrisomgr  44055