Theorem imaeq1 6084

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 6003	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5963	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5713	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5713	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2805	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1537  ran crn 5701   ↾ cres 5702   “ cima 5703

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-3an 1089  df-tru 1540  df-fal 1550  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-rab 3444  df-v 3490  df-dif 3979  df-un 3981  df-in 3983  df-ss 3993  df-nul 4353  df-if 4549  df-sn 4649  df-pr 4651  df-op 4655  df-br 5167  df-opab 5229  df-cnv 5708  df-dm 5710  df-rn 5711  df-res 5712  df-ima 5713

This theorem is referenced by:  imaeq1i  6086  imaeq1d  6088  suppval  8203  naddcllem  8732  eceq2  8804  marypha1lem  9502  marypha1  9503  ackbij2lem2  10308  ackbij2lem3  10309  r1om  10312  limsupval  15520  isacs1i  17715  mreacs  17716  islindf  21855  iscnp  23266  xkoccn  23648  xkohaus  23682  xkoco1cn  23686  xkoco2cn  23687  xkococnlem  23688  xkococn  23689  xkoinjcn  23716  fmval  23972  fmf  23974  utoptop  24264  restutop  24267  restutopopn  24268  ustuqtoplem  24269  ustuqtop1  24271  ustuqtop2  24272  ustuqtop4  24274  ustuqtop5  24275  utopsnneiplem  24277  utopsnnei  24279  neipcfilu  24326  psmetutop  24601  cfilfval  25317  elply2  26255  coeeu  26284  coelem  26285  coeeq  26286  dmarea  27018  negsval  28075  mclsax  35537  tailfval  36338  bj-cleq  36928  bj-funun  37218  poimirlem15  37595  poimirlem24  37604  brtrclfv2  43689  liminfval  45680  ushggricedg  47780  uhgrimisgrgric  47783