Theorem imaeq1 6047

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 5964	. . 3 ⊢ (𝐴 = 𝐵 → (𝐴 ↾ 𝐶) = (𝐵 ↾ 𝐶))
2	1	rneqd 5920	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐴 ↾ 𝐶) = ran (𝐵 ↾ 𝐶))
3		df-ima 5664	. 2 ⊢ (𝐴 “ 𝐶) = ran (𝐴 ↾ 𝐶)
4		df-ima 5664	. 2 ⊢ (𝐵 “ 𝐶) = ran (𝐵 ↾ 𝐶)
5	2, 3, 4	3eqtr4g 2821	1 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

This proof depends on syntax axioms:   → wi 4   = wceq 1570  ran crn 5652   ↾ cres 5653   “ cima 5654

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 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

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 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3453  df-dif 3902  df-un 3904  df-in 3906  df-ss 3916  df-nul 4280  df-if 4483  df-sn 4585  df-pr 4587  df-op 4591  df-br 5104  df-opab 5168  df-cnv 5659  df-dm 5661  df-rn 5662  df-res 5663  df-ima 5664

This theorem is used by:  imaeq1i  6049  imaeq1d  6051  suppval  8172  naddcllem  8678  eceq2  8752  marypha1lem  9418  marypha1  9419  ackbij2lem2  10310  ackbij2lem3  10311  hfom  10314  limsupval  15634  isacs1i  17824  mreacs  17825  islindf  22111  iscnp  23548  xkoccn  23931  xkohaus  23965  xkoco1cn  23969  xkoco2cn  23970  xkococnlem  23971  xkococn  23972  xkoinjcn  23999  fmval  24255  fmf  24257  utoptop  24546  restutop  24549  restutopopn  24550  ustuqtoplem  24551  ustuqtop1  24553  ustuqtop2  24554  ustuqtop4  24556  ustuqtop5  24557  utopsnneiplem  24559  utopsnnei  24561  neipcfilu  24607  psmetutop  24879  cfilfval  25578  elply2  26507  coeeu  26537  coelem  26538  coeeq  26539  dmarea  27278  negsval  28404  mclsax  36313  tailfval  37140  bj-cleq  37855  bj-funun  38153  poimirlem15  38533  poimirlem24  38542  brtrclfv2  44712  liminfval  46738  ushggricedg  48994  uhgrimisgrgric  48998