Theorem imaeq2 6043

Description: Equality theorem for image. (Contributed by NM, 14-Aug-1994.)

Assertion

Ref	Expression
imaeq2	⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2

Step	Hyp	Ref	Expression
1		reseq2 5961	. . 3 ⊢ (𝐴 = 𝐵 → (𝐶 ↾ 𝐴) = (𝐶 ↾ 𝐵))
2	1	rneqd 5918	. 2 ⊢ (𝐴 = 𝐵 → ran (𝐶 ↾ 𝐴) = ran (𝐶 ↾ 𝐵))
3		df-ima 5667	. 2 ⊢ (𝐶 “ 𝐴) = ran (𝐶 ↾ 𝐴)
4		df-ima 5667	. 2 ⊢ (𝐶 “ 𝐵) = ran (𝐶 ↾ 𝐵)
5	2, 3, 4	3eqtr4g 2795	1 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1540  ran crn 5655   ↾ cres 5656   “ cima 5657

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2707

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2065  df-clab 2714  df-cleq 2727  df-clel 2809  df-rab 3416  df-v 3461  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-sn 4602  df-pr 4604  df-op 4608  df-br 5120  df-opab 5182  df-xp 5660  df-cnv 5662  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667

This theorem is referenced by:  imaeq2i  6045  imaeq2d  6047  relimasn  6072  cnvimassrndm  6141  funimaexgOLD  6624  fimadmfo  6799  ssimaex  6964  ssimaexg  6965  isoselem  7334  isowe2  7343  f1opw2  7662  mptcnfimad  7985  fnse  8132  supp0cosupp0  8207  tz7.49  8459  ecexr  8724  fopwdom  9094  sbthlem2  9098  sbth  9107  ssenen  9165  sbthfi  9213  fodomfi  9322  imafiOLD  9326  domunfican  9333  fodomfiOLD  9342  f1opwfi  9368  fipreima  9370  marypha1lem  9445  ordtypelem2  9533  ordtypelem3  9534  ordtypelem9  9540  dfac12lem2  10159  dfac12r  10161  ackbij2lem2  10253  ackbij2lem3  10254  r1om  10257  enfin2i  10335  zorn2lem6  10515  zorn2lem7  10516  isacs5lem  18555  acsdrscl  18556  gicsubgen  19262  ghmqusnsglem1  19263  ghmquskerlem1  19266  ghmquskerco  19267  gicqusker  19271  efgrelexlema  19730  tgcn  23190  subbascn  23192  iscnp4  23201  cnpnei  23202  cnima  23203  iscncl  23207  cncls  23212  cnconst2  23221  cnrest2  23224  cnprest  23227  cnindis  23230  cncmp  23330  cmpfi  23346  2ndcomap  23396  ptbasfi  23519  xkoopn  23527  xkoccn  23557  txcnp  23558  ptcnplem  23559  txcnmpt  23562  ptrescn  23577  xkoco1cn  23595  xkoco2cn  23596  xkococn  23598  xkoinjcn  23625  elqtop  23635  qtopomap  23656  qtopcmap  23657  ordthmeolem  23739  fbasrn  23822  elfm  23885  elfm2  23886  elfm3  23888  imaelfm  23889  rnelfmlem  23890  rnelfm  23891  fmfnfmlem2  23893  fmfnfmlem3  23894  fmfnfmlem4  23895  fmco  23899  flffbas  23933  lmflf  23943  fcfneii  23975  ptcmplem3  23992  ptcmplem5  23994  ptcmpg  23995  cnextcn  24005  symgtgp  24044  ghmcnp  24053  eltsms  24071  tsmsf1o  24083  fmucnd  24230  ucnextcn  24242  metcnp3  24479  mbfdm  25579  ismbf  25581  mbfima  25583  ismbfd  25592  mbfimaopnlem  25608  mbfimaopn2  25610  i1fd  25634  ellimc2  25830  limcflf  25834  xrlimcnp  26930  oldval  27814  ubthlem1  30851  disjpreima  32565  imadifxp  32582  preimane  32648  fnpreimac  32649  lmicqusker  33433  ricqusker  33442  algextdeglem4  33754  algextdeg  33759  qtophaus  33867  rhmpreimacnlem  33915  rrhre  34052  mbfmcnvima  34287  imambfm  34294  eulerpartgbij  34404  erdszelem1  35213  erdsze  35224  erdsze2lem2  35226  cvmscbv  35280  cvmsi  35287  cvmsval  35288  cvmliftlem15  35320  opelco3  35792  brimageg  35945  fnimage  35947  imageval  35948  fvimage  35949  filnetlem4  36399  bj-imdirval3  37202  bj-imdirco  37208  ptrest  37643  ismtyhmeolem  37828  ismtybndlem  37830  heibor1lem  37833  zndvdchrrhm  41985  aks6d1c7lem2  42194  aks5lem4a  42203  lmhmfgima  43108  brtrclfv2  43751  csbfv12gALTVD  44923  icccncfext  45916  sge0f1o  46411  smfresal  46817  smfpimbor1lem1  46827  smfpimbor1lem2  46828  smfco  46831  f1cof1b  47106  fnfocofob  47108  imaelsetpreimafv  47409  fundcmpsurinjlem3  47414  imasetpreimafvbijlemfo  47419  fundcmpsurbijinjpreimafv  47421  grimco  47902  uhgrimedgi  47903  isuspgrim0  47907  isuspgrimlem  47908  upgrimwlklem5  47914  gricushgr  47930  grimedg  47948  grtrimap  47960  isubgr3stgrlem5  47982  isubgr3stgrlem6  47983  isubgr3stgrlem7  47984  isubgr3stgrlem8  47985  uspgrlimlem4  48003  grlimgrtrilem2  48007