Theorem imaeq1 6065

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 5980	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5932	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5671	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5671	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2823	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5659   ↾ cres 5660   “ cima 5661

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-3an 1105  df-tru 1573  df-fal 1583  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-rab 3417  df-v 3456  df-ss 3901  df-dif 4050  df-in 4094  df-un 4154  df-nul 4282  df-if 4486  df-sn 4589  df-pr 4591  df-op 4841  df-br 5109  df-opab 5174  df-cnv 5666  df-dm 5668  df-rn 5669  df-res 5670  df-ima 5671

This theorem is used by:  imaeq1i  6067  imaeq1d  6069  suppval  8216  naddcllem  8723  eceq2  8797  marypha1lem  9462  marypha1  9463  ackbij2lem2  10356  ackbij2lem3  10357  hfom  10360  limsupval  15685  isacs1i  17881  mreacs  17882  islindf  22173  iscnp  23610  xkoccn  23993  xkohaus  24027  xkoco1cn  24031  xkoco2cn  24032  xkococnlem  24033  xkococn  24034  xkoinjcn  24061  fmval  24317  fmf  24319  utoptop  24608  restutop  24611  restutopopn  24612  ustuqtoplem  24613  ustuqtop1  24615  ustuqtop2  24616  ustuqtop4  24618  ustuqtop5  24619  utopsnneiplem  24621  utopsnnei  24623  neipcfilu  24669  psmetutop  24941  cfilfval  25640  elply2  26569  coeeu  26599  coelem  26600  coeeq  26601  dmarea  27342  negsval  28468  mclsax  36542  tailfval  37375  bj-cleq  38090  bj-funun  38441  poimirlem15  38821  poimirlem24  38830  brtrclfv2  44988  ackbij3  46289  liminfval  47042  ushggricedg  49298  uhgrimisgrgric  49302