Theorem imaeq2d 6019

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

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

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 2708

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 2715  df-cleq 2728  df-clel 2811  df-rab 3400  df-v 3442  df-dif 3904  df-un 3906  df-in 3908  df-ss 3918  df-nul 4286  df-if 4480  df-sn 4581  df-pr 4583  df-op 4587  df-br 5099  df-opab 5161  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaeq12d  6020  nfimad  6028  csbima12  6038  elimasni  6050  inisegn0  6057  csbrn  6161  ressn  6243  csbpredg  6265  predprc  6296  fncofn  6609  foima  6751  focnvimacdmdm  6758  f1imacnv  6790  dffv3  6830  fvco2  6931  sspreima  7013  fimacnvinrn2  7017  rescnvimafod  7018  fsn2  7081  funfvima3  7182  isofrlem  7286  isoselem  7287  fnexALT  7895  mptcnfimad  7930  curry1  8046  curry2  8049  fparlem3  8056  fparlem4  8057  suppsnop  8120  ressuppssdif  8127  suppco  8148  imacosupp  8151  naddcllem  8604  eceq1  8674  uniqs2  8714  ecinxp  8729  mapsnd  8824  sbthlem2  9016  sbth  9025  sbthfi  9123  phplem2  9129  php3  9133  marypha1lem  9336  cantnfp1lem3  9589  tcrank  9796  fin4en1  10219  fin1a2lem7  10316  hsmexlem4  10339  hsmexlem5  10340  fpwwe2cbv  10541  fpwwe2lem3  10544  fpwwe2lem12  10553  fpwwecbv  10555  canth4  10558  resunimafz0  14368  limsupgval  15399  isercoll  15591  vdwlem1  16909  vdwlem6  16914  vdwlem7  16915  vdwlem8  16916  vdwlem12  16920  vdwlem13  16921  vdwnn  16926  0ram  16948  ramz2  16952  isacs1i  17580  acsficl  18470  gsumvalx  18601  gsumpropd  18603  gsumpropd2lem  18604  gsumress  18607  efgrelexlema  19678  gsumval3a  19832  gsumval3lem1  19834  gsum2dlem2  19900  gsum2d2  19903  dprddisj  19940  dprdf1o  19963  dprdsn  19967  dprd2dlem2  19971  dprd2dlem1  19972  dprd2da  19973  dprd2db  19974  dmdprdsplit2lem  19976  dpjfval  19986  rngqiprngimf1  21255  frlmup3  21755  islindf  21767  islindf2  21769  lindfind  21771  f1lindf  21777  lmimlbs  21791  coe1mul2lem2  22210  subbascn  23198  cncls2  23217  cncls  23218  cnntr  23219  cnpresti  23232  cnprest  23233  cnt1  23294  cnhaus  23298  cncmp  23336  cnconn  23366  1stcfb  23389  xkoccn  23563  ptrescn  23583  xkococnlem  23603  qtopeu  23660  qtoprest  23661  kqdisj  23676  kqcldsat  23677  ordthmeolem  23745  fmfnfmlem4  23901  ustuqtoplem  24183  utopsnneiplem  24191  utopsnneip  24192  ucncn  24228  metustto  24497  metustexhalf  24500  metustfbas  24501  cfilucfil  24503  metuust  24504  cfilucfil2  24505  metuel  24508  metuel2  24509  psmetutop  24511  restmetu  24514  metucn  24515  pi1addval  25004  iscph  25126  cphsscph  25207  uniioombllem3  25542  dyadmbl  25557  mbfima  25587  mbfimaicc  25588  mbfimasn  25589  ismbfd  25596  ismbf2d  25597  ismbf3d  25611  mbfimaopnlem  25612  i1fd  25638  i1f1  25647  itg11  25648  i1faddlem  25650  i1fmullem  25651  i1fadd  25652  itg1addlem3  25655  itg1mulc  25661  itg2gt0  25717  limcnlp  25835  ellimc3  25836  limcflf  25838  limciun  25851  mdegval  26024  mdeg0  26031  mdegvsca  26037  mdegpropd  26045  deg1val  26057  ig1pval  26137  coeeu  26186  coeeq  26188  pserulm  26387  areambl  26924  cutsval  27776  madeval  27828  addbday  28014  negsval  28021  bdayons  28272  zcuts0  28404  bdaypw2n0bndlem  28459  dfpth2  29802  pthdlem2  29841  cyclnumvtx  29873  eupth2lem3  30311  eupth2  30314  issh  31283  isch  31297  shsval  31387  2ndimaxp  32724  fnpreimac  32749  dfcnv2  32754  mptiffisupp  32772  indsupp  32949  indfsid  32951  s2rnOLD  33026  s3rnOLD  33028  swrdrndisj  33039  pwrssmgc  33082  gsummpt2co  33131  gsumpart  33146  gsumhashmul  33150  cycpmco2rn  33207  qusrn  33490  elrspunidl  33509  rhmimaidl  33513  r1pquslmic  33692  psrbasfsupp  33693  esplyfval  33721  esplyfval0  33722  esplyfval2  33723  vieta  33736  dimval  33757  dimvalfi  33758  ply1degltdimlem  33779  extdgval  33810  algextdeglem3  33876  algextdeglem4  33877  algextdeglem5  33878  smatrcl  33953  locfinreflem  33997  zarclsint  34029  rhmpreimacn  34042  zrhunitpreima  34133  mbfmco2  34422  sibfima  34495  sibfof  34497  eulerpartlemgv  34530  eulerpartlemn  34538  eulerpart  34539  orvcval4  34618  orvcelval  34626  orvcelel  34627  ballotlemscr  34676  fnrelpredd  35247  fineqvr1ombregs  35294  f1resfz0f1d  35308  pthhashvtx  35322  erdszelem3  35387  erdsze  35396  cvmliftlem3  35481  cvmliftlem7  35485  cvmlift2lem9a  35497  msrval  35732  mvtinf  35749  mclsval  35757  mclsax  35763  mthmpps  35776  opelco3  35969  funpartlem  36136  tailval  36567  ptrest  37820  poimirlem1  37822  poimirlem2  37823  poimirlem3  37824  poimirlem4  37825  poimirlem5  37826  poimirlem6  37827  poimirlem7  37828  poimirlem9  37830  poimirlem10  37831  poimirlem11  37832  poimirlem12  37833  poimirlem13  37834  poimirlem14  37835  poimirlem15  37836  poimirlem16  37837  poimirlem17  37838  poimirlem19  37840  poimirlem20  37841  poimirlem22  37843  poimirlem23  37844  poimirlem24  37845  poimirlem25  37846  poimirlem26  37847  poimirlem27  37848  poimirlem28  37849  poimirlem29  37850  poimirlem31  37852  poimirlem32  37853  mblfinlem2  37859  volsupnfl  37866  itg2addnclem2  37873  sstotbnd2  37975  ismtyhmeolem  38005  grpokerinj  38094  lkrfval  39347  aks6d1c6lem5  42431  aks6d1c7lem3  42436  dnnumch3lem  43288  aomclem8  43303  pwfi2f1o  43338  cytpval  43444  frege97d  43993  frege109d  43998  frege131d  44005  nzprmdif  44560  relpfrlem  45194  wessf1ornlem  45429  limsuplesup  45943  limsupvaluz  45952  limsuplt2  45997  limsupge  46005  liminfgval  46006  liminfval2  46012  liminflelimsuplem  46019  liminflelimsup  46020  preimaioomnf  46963  fcoreslem2  47310  f1cof1blem  47320  3f1oss1  47321  afv2co2  47503  imarnf1pr  47528  preimafvelsetpreimafv  47634  imaelsetpreimafv  47641  imasetpreimafvbijlemfo  47651  fundcmpsurbijinjpreimafv  47653  fundcmpsurinj  47655  fundcmpsurbijinj  47656  isgrim  48128  grimuhgr  48133  grimcnv  48134  grimco  48135  uhgrimedgi  48136  isuspgrim0lem  48139  isuspgrim0  48140  upgrimwlklem3  48145  upgrimtrls  48152  upgrimpths  48155  gricushgr  48163  cycldlenngric  48174  isubgrgrim  48175  uhgrimisgrgriclem  48176  clnbgrgrimlem  48179  clnbgrgrim  48180  grimedg  48181  cycl3grtri  48193  isubgr3stgrlem4  48215  uspgrlimlem3  48236  predisj  49056  imasubclem3  49351