Theorem imaeq1 5602

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 5528	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5491	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5262	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5262	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2830	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1631  ran crn 5250   ↾ cres 5251   “ cima 5252

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751

This theorem depends on definitions:  df-bi 197  df-an 383  df-or 835  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-rab 3070  df-v 3353  df-dif 3726  df-un 3728  df-in 3730  df-ss 3737  df-nul 4064  df-if 4226  df-sn 4317  df-pr 4319  df-op 4323  df-br 4787  df-opab 4847  df-cnv 5257  df-dm 5259  df-rn 5260  df-res 5261  df-ima 5262

This theorem is referenced by:  imaeq1i  5604  imaeq1d  5606  suppval  7448  eceq2  7936  marypha1lem  8495  marypha1  8496  ackbij2lem2  9264  ackbij2lem3  9265  r1om  9268  limsupval  14413  isacs1i  16525  mreacs  16526  islindf  20368  iscnp  21262  xkoccn  21643  xkohaus  21677  xkoco1cn  21681  xkoco2cn  21682  xkococnlem  21683  xkococn  21684  xkoinjcn  21711  fmval  21967  fmf  21969  utoptop  22258  restutop  22261  restutopopn  22262  ustuqtoplem  22263  ustuqtop1  22265  ustuqtop2  22266  ustuqtop4  22268  ustuqtop5  22269  utopsnneiplem  22271  utopsnnei  22273  neipcfilu  22320  psmetutop  22592  cfilfval  23281  elply2  24172  coeeu  24201  coelem  24202  coeeq  24203  dmarea  24905  mclsax  31804  tailfval  32704  bj-cleq  33280  poimirlem15  33757  poimirlem24  33766  brtrclfv2  38545  liminfval  40509