Theorem imaeq1 5891

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 5812	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5772	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5532	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5532	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2858	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1538  ran crn 5520   ↾ cres 5521   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  imaeq1i  5893  imaeq1d  5895  suppval  7815  eceq2  8312  marypha1lem  8881  marypha1  8882  ackbij2lem2  9651  ackbij2lem3  9652  r1om  9655  limsupval  14823  isacs1i  16920  mreacs  16921  islindf  20501  iscnp  21842  xkoccn  22224  xkohaus  22258  xkoco1cn  22262  xkoco2cn  22263  xkococnlem  22264  xkococn  22265  xkoinjcn  22292  fmval  22548  fmf  22550  utoptop  22840  restutop  22843  restutopopn  22844  ustuqtoplem  22845  ustuqtop1  22847  ustuqtop2  22848  ustuqtop4  22850  ustuqtop5  22851  utopsnneiplem  22853  utopsnnei  22855  neipcfilu  22902  psmetutop  23174  cfilfval  23868  elply2  24793  coeeu  24822  coelem  24823  coeeq  24824  dmarea  25543  mclsax  32929  tailfval  33833  bj-cleq  34398  bj-funun  34667  poimirlem15  35072  poimirlem24  35081  brtrclfv2  40428  liminfval  42401  isomgreqve  44343  isomgrsym  44354  isomgrtr  44357  ushrisomgr  44359