Theorem imaeq2d 6016

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 6012	. 2 ⊢ (𝐴 = 𝐵 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1541   “ cima 5624

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1544  df-fal 1554  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-rab 3397  df-v 3439  df-dif 3901  df-un 3903  df-in 3905  df-ss 3915  df-nul 4283  df-if 4477  df-sn 4578  df-pr 4580  df-op 4584  df-br 5096  df-opab 5158  df-xp 5627  df-cnv 5629  df-dm 5631  df-rn 5632  df-res 5633  df-ima 5634

This theorem is referenced by:  imaeq12d  6017  nfimad  6025  csbima12  6035  elimasni  6047  inisegn0  6054  csbrn  6158  ressn  6240  csbpredg  6262  predprc  6293  fncofn  6606  foima  6748  focnvimacdmdm  6755  f1imacnv  6787  dffv3  6827  fvco2  6928  sspreima  7010  fimacnvinrn2  7014  rescnvimafod  7015  fsn2  7078  funfvima3  7179  isofrlem  7283  isoselem  7284  fnexALT  7892  mptcnfimad  7927  curry1  8043  curry2  8046  fparlem3  8053  fparlem4  8054  suppsnop  8117  ressuppssdif  8124  suppco  8145  imacosupp  8148  naddcllem  8600  eceq1  8670  uniqs2  8710  ecinxp  8725  mapsnd  8820  sbthlem2  9012  sbth  9021  sbthfi  9119  phplem2  9125  php3  9129  marypha1lem  9328  cantnfp1lem3  9581  tcrank  9788  fin4en1  10211  fin1a2lem7  10308  hsmexlem4  10331  hsmexlem5  10332  fpwwe2cbv  10532  fpwwe2lem3  10535  fpwwe2lem12  10544  fpwwecbv  10546  canth4  10549  resunimafz0  14359  limsupgval  15390  isercoll  15582  vdwlem1  16900  vdwlem6  16905  vdwlem7  16906  vdwlem8  16907  vdwlem12  16911  vdwlem13  16912  vdwnn  16917  0ram  16939  ramz2  16943  isacs1i  17571  acsficl  18461  gsumvalx  18592  gsumpropd  18594  gsumpropd2lem  18595  gsumress  18598  efgrelexlema  19669  gsumval3a  19823  gsumval3lem1  19825  gsum2dlem2  19891  gsum2d2  19894  dprddisj  19931  dprdf1o  19954  dprdsn  19958  dprd2dlem2  19962  dprd2dlem1  19963  dprd2da  19964  dprd2db  19965  dmdprdsplit2lem  19967  dpjfval  19977  rngqiprngimf1  21246  frlmup3  21746  islindf  21758  islindf2  21760  lindfind  21762  f1lindf  21768  lmimlbs  21782  coe1mul2lem2  22201  subbascn  23189  cncls2  23208  cncls  23209  cnntr  23210  cnpresti  23223  cnprest  23224  cnt1  23285  cnhaus  23289  cncmp  23327  cnconn  23357  1stcfb  23380  xkoccn  23554  ptrescn  23574  xkococnlem  23594  qtopeu  23651  qtoprest  23652  kqdisj  23667  kqcldsat  23668  ordthmeolem  23736  fmfnfmlem4  23892  ustuqtoplem  24174  utopsnneiplem  24182  utopsnneip  24183  ucncn  24219  metustto  24488  metustexhalf  24491  metustfbas  24492  cfilucfil  24494  metuust  24495  cfilucfil2  24496  metuel  24499  metuel2  24500  psmetutop  24502  restmetu  24505  metucn  24506  pi1addval  24995  iscph  25117  cphsscph  25198  uniioombllem3  25533  dyadmbl  25548  mbfima  25578  mbfimaicc  25579  mbfimasn  25580  ismbfd  25587  ismbf2d  25588  ismbf3d  25602  mbfimaopnlem  25603  i1fd  25629  i1f1  25638  itg11  25639  i1faddlem  25641  i1fmullem  25642  i1fadd  25643  itg1addlem3  25646  itg1mulc  25652  itg2gt0  25708  limcnlp  25826  ellimc3  25827  limcflf  25829  limciun  25842  mdegval  26015  mdeg0  26022  mdegvsca  26028  mdegpropd  26036  deg1val  26048  ig1pval  26128  coeeu  26177  coeeq  26179  pserulm  26378  areambl  26915  scutval  27761  madeval  27813  addsbday  27980  negsval  27987  bdayon  28229  dfpth2  29728  pthdlem2  29767  cyclnumvtx  29799  eupth2lem3  30237  eupth2  30240  issh  31209  isch  31223  shsval  31313  2ndimaxp  32650  fnpreimac  32675  dfcnv2  32680  mptiffisupp  32698  indsupp  32877  indfsid  32879  s2rnOLD  32954  s3rnOLD  32956  swrdrndisj  32967  pwrssmgc  33010  gsummpt2co  33059  gsumpart  33074  gsumhashmul  33078  cycpmco2rn  33135  qusrn  33418  elrspunidl  33437  rhmimaidl  33441  r1pquslmic  33620  psrbasfsupp  33621  esplyfval  33649  esplyfval0  33650  esplyfval2  33651  vieta  33664  dimval  33685  dimvalfi  33686  ply1degltdimlem  33707  extdgval  33738  algextdeglem3  33804  algextdeglem4  33805  algextdeglem5  33806  smatrcl  33881  locfinreflem  33925  zarclsint  33957  rhmpreimacn  33970  zrhunitpreima  34061  mbfmco2  34350  sibfima  34423  sibfof  34425  eulerpartlemgv  34458  eulerpartlemn  34466  eulerpart  34467  orvcval4  34546  orvcelval  34554  orvcelel  34555  ballotlemscr  34604  fnrelpredd  35174  fineqvr1ombregs  35207  f1resfz0f1d  35230  pthhashvtx  35244  erdszelem3  35309  erdsze  35318  cvmliftlem3  35403  cvmliftlem7  35407  cvmlift2lem9a  35419  msrval  35654  mvtinf  35671  mclsval  35679  mclsax  35685  mthmpps  35698  opelco3  35891  funpartlem  36058  tailval  36489  ptrest  37732  poimirlem1  37734  poimirlem2  37735  poimirlem3  37736  poimirlem4  37737  poimirlem5  37738  poimirlem6  37739  poimirlem7  37740  poimirlem9  37742  poimirlem10  37743  poimirlem11  37744  poimirlem12  37745  poimirlem13  37746  poimirlem14  37747  poimirlem15  37748  poimirlem16  37749  poimirlem17  37750  poimirlem19  37752  poimirlem20  37753  poimirlem22  37755  poimirlem23  37756  poimirlem24  37757  poimirlem25  37758  poimirlem26  37759  poimirlem27  37760  poimirlem28  37761  poimirlem29  37762  poimirlem31  37764  poimirlem32  37765  mblfinlem2  37771  volsupnfl  37778  itg2addnclem2  37785  sstotbnd2  37887  ismtyhmeolem  37917  grpokerinj  38006  lkrfval  39259  aks6d1c6lem5  42343  aks6d1c7lem3  42348  dnnumch3lem  43203  aomclem8  43218  pwfi2f1o  43253  cytpval  43359  frege97d  43909  frege109d  43914  frege131d  43921  nzprmdif  44476  relpfrlem  45110  wessf1ornlem  45345  limsuplesup  45859  limsupvaluz  45868  limsuplt2  45913  limsupge  45921  liminfgval  45922  liminfval2  45928  liminflelimsuplem  45935  liminflelimsup  45936  preimaioomnf  46879  fcoreslem2  47226  f1cof1blem  47236  3f1oss1  47237  afv2co2  47419  imarnf1pr  47444  preimafvelsetpreimafv  47550  imaelsetpreimafv  47557  imasetpreimafvbijlemfo  47567  fundcmpsurbijinjpreimafv  47569  fundcmpsurinj  47571  fundcmpsurbijinj  47572  isgrim  48044  grimuhgr  48049  grimcnv  48050  grimco  48051  uhgrimedgi  48052  isuspgrim0lem  48055  isuspgrim0  48056  upgrimwlklem3  48061  upgrimtrls  48068  upgrimpths  48071  gricushgr  48079  cycldlenngric  48090  isubgrgrim  48091  uhgrimisgrgriclem  48092  clnbgrgrimlem  48095  clnbgrgrim  48096  grimedg  48097  cycl3grtri  48109  isubgr3stgrlem4  48131  uspgrlimlem3  48152  predisj  48972  imasubclem3  49267