Theorem imaeq1 5620

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

Syntax hints:   → wi 4   = wceq 1632  ran crn 5268   ↾ cres 5269   “ cima 5270

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1989  ax-6 2055  ax-7 2091  ax-9 2149  ax-10 2169  ax-11 2184  ax-12 2197  ax-13 2392  ax-ext 2741

This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2048  df-clab 2748  df-cleq 2754  df-clel 2757  df-nfc 2892  df-rab 3060  df-v 3343  df-dif 3719  df-un 3721  df-in 3723  df-ss 3730  df-nul 4060  df-if 4232  df-sn 4323  df-pr 4325  df-op 4329  df-br 4806  df-opab 4866  df-cnv 5275  df-dm 5277  df-rn 5278  df-res 5279  df-ima 5280

This theorem is referenced by:  imaeq1i  5622  imaeq1d  5624  suppval  7467  eceq2  7954  marypha1lem  8507  marypha1  8508  ackbij2lem2  9275  ackbij2lem3  9276  r1om  9279  limsupval  14425  isacs1i  16540  mreacs  16541  islindf  20374  iscnp  21264  xkoccn  21645  xkohaus  21679  xkoco1cn  21683  xkoco2cn  21684  xkococnlem  21685  xkococn  21686  xkoinjcn  21713  fmval  21969  fmf  21971  utoptop  22260  restutop  22263  restutopopn  22264  ustuqtoplem  22265  ustuqtop1  22267  ustuqtop2  22268  ustuqtop4  22270  ustuqtop5  22271  utopsnneiplem  22273  utopsnnei  22275  neipcfilu  22322  psmetutop  22594  cfilfval  23283  elply2  24172  coeeu  24201  coelem  24202  coeeq  24203  dmarea  24905  mclsax  31795  tailfval  32695  bj-cleq  33274  poimirlem15  33756  poimirlem24  33765  brtrclfv2  38540  liminfval  40513