Theorem imaeq2d 5958

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq2d	⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Proof of Theorem imaeq2d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq2 5954	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   “ cima 5583

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-3an 1087  df-tru 1542  df-fal 1552  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-rab 3072  df-v 3424  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4254  df-if 4457  df-sn 4559  df-pr 4561  df-op 4565  df-br 5071  df-opab 5133  df-xp 5586  df-cnv 5588  df-dm 5590  df-rn 5591  df-res 5592  df-ima 5593

This theorem is referenced by:  imaeq12d  5959  nfimad  5967  csbima12  5976  elimasngOLD  5987  elimasni  5988  inisegn0  5995  csbrn  6095  ressn  6177  csbpredg  6197  fncofn  6532  foima  6677  focnvimacdmdm  6684  f1imacnv  6716  dffv3  6752  fvco2  6847  sspreima  6927  fimacnvinrn2  6932  rescnvimafod  6933  fsn2  6990  funfvima3  7094  isofrlem  7191  isoselem  7192  fnexALT  7767  curry1  7915  curry2  7918  fparlem3  7925  fparlem4  7926  suppsnop  7965  ressuppssdif  7972  suppco  7993  imacosupp  7996  eceq1  8494  uniqs2  8526  ecinxp  8539  mapsnd  8632  sbthlem2  8824  sbth  8833  phplem4  8895  php3  8899  sbthfi  8942  marypha1lem  9122  cantnfp1lem3  9368  tcrank  9573  fin4en1  9996  fin1a2lem7  10093  hsmexlem4  10116  hsmexlem5  10117  fpwwe2cbv  10317  fpwwe2lem3  10320  fpwwe2lem12  10329  fpwwecbv  10331  canth4  10334  resunimafz0  14085  limsupgval  15113  isercoll  15307  vdwlem1  16610  vdwlem6  16615  vdwlem7  16616  vdwlem8  16617  vdwlem12  16621  vdwlem13  16622  vdwnn  16627  0ram  16649  ramz2  16653  isacs1i  17283  acsficl  18180  gsumvalx  18275  gsumpropd  18277  gsumpropd2lem  18278  gsumress  18281  efgrelexlema  19270  gsumval3a  19419  gsumval3lem1  19421  gsum2dlem2  19487  gsum2d2  19490  dprddisj  19527  dprdf1o  19550  dprdsn  19554  dprd2dlem2  19558  dprd2dlem1  19559  dprd2da  19560  dprd2db  19561  dmdprdsplit2lem  19563  dpjfval  19573  frlmup3  20917  islindf  20929  islindf2  20931  lindfind  20933  f1lindf  20939  lmimlbs  20953  coe1mul2lem2  21349  subbascn  22313  cncls2  22332  cncls  22333  cnntr  22334  cnpresti  22347  cnprest  22348  cnt1  22409  cnhaus  22413  cncmp  22451  cnconn  22481  1stcfb  22504  xkoccn  22678  ptrescn  22698  xkococnlem  22718  qtopeu  22775  qtoprest  22776  kqdisj  22791  kqcldsat  22792  ordthmeolem  22860  fmfnfmlem4  23016  ustuqtoplem  23299  utopsnneiplem  23307  utopsnneip  23308  ucncn  23345  metustto  23615  metustexhalf  23618  metustfbas  23619  cfilucfil  23621  metuust  23622  cfilucfil2  23623  metuel  23626  metuel2  23627  psmetutop  23629  restmetu  23632  metucn  23633  pi1addval  24117  iscph  24239  cphsscph  24320  uniioombllem3  24654  dyadmbl  24669  mbfima  24699  mbfimaicc  24700  mbfimasn  24701  ismbfd  24708  ismbf2d  24709  ismbf3d  24723  mbfimaopnlem  24724  i1fd  24750  i1f1  24759  itg11  24760  i1faddlem  24762  i1fmullem  24763  i1fadd  24764  itg1addlem3  24767  itg1mulc  24774  itg2gt0  24830  limcnlp  24947  ellimc3  24948  limcflf  24950  limciun  24963  mdegval  25133  mdeg0  25140  mdegvsca  25146  mdegpropd  25154  deg1val  25166  ig1pval  25242  coeeu  25291  coeeq  25293  pserulm  25486  areambl  26013  pthdlem2  28037  eupth2lem3  28501  eupth2  28504  issh  29471  isch  29485  shsval  29575  2ndimaxp  30885  fnpreimac  30910  dfcnv2  30915  s2rn  31120  s3rn  31122  swrdrndisj  31131  pwrssmgc  31180  gsummpt2co  31210  gsumpart  31217  gsumhashmul  31218  cycpmco2rn  31294  elrspunidl  31508  rhmimaidl  31511  dimval  31588  dimvalfi  31589  extdgval  31631  smatrcl  31648  locfinreflem  31692  zarclsint  31724  rhmpreimacn  31737  zrhunitpreima  31828  mbfmco2  32132  sibfima  32205  sibfof  32207  eulerpartlemgv  32240  eulerpartlemn  32248  eulerpart  32249  orvcval4  32327  orvcelval  32335  orvcelel  32336  ballotlemscr  32385  fnrelpredd  32961  f1resfz0f1d  32972  pthhashvtx  32989  erdszelem3  33055  erdsze  33064  cvmliftlem3  33149  cvmliftlem7  33153  cvmlift2lem9a  33165  msrval  33400  mvtinf  33417  mclsval  33425  mclsax  33431  mthmpps  33444  opelco3  33655  naddcllem  33758  scutval  33921  madeval  33963  negsval  34050  funpartlem  34171  tailval  34489  ptrest  35703  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem5  35709  poimirlem6  35710  poimirlem7  35711  poimirlem9  35713  poimirlem10  35714  poimirlem11  35715  poimirlem12  35716  poimirlem13  35717  poimirlem14  35718  poimirlem15  35719  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem22  35726  poimirlem23  35727  poimirlem24  35728  poimirlem25  35729  poimirlem26  35730  poimirlem27  35731  poimirlem28  35732  poimirlem29  35733  poimirlem31  35735  poimirlem32  35736  mblfinlem2  35742  volsupnfl  35749  itg2addnclem2  35756  sstotbnd2  35859  ismtyhmeolem  35889  grpokerinj  35978  lkrfval  37028  dnnumch3lem  40787  aomclem8  40802  pwfi2f1o  40837  cytpval  40950  frege97d  41249  frege109d  41254  frege131d  41261  nzprmdif  41826  wessf1ornlem  42611  limsuplesup  43130  limsupvaluz  43139  limsuplt2  43184  limsupge  43192  liminfgval  43193  liminfval2  43199  liminflelimsuplem  43206  liminflelimsup  43207  preimaioomnf  44143  fcoreslem2  44445  f1cof1blem  44455  afv2co2  44636  imarnf1pr  44661  preimafvelsetpreimafv  44728  imaelsetpreimafv  44735  imasetpreimafvbijlemfo  44745  fundcmpsurbijinjpreimafv  44747  fundcmpsurinj  44749  fundcmpsurbijinj  44750  isomgr  45163  isomushgr  45166  isomgrsym  45176  isomgrtrlem  45178  predisj  46044