Theorem imaeq2d 6045

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

Syntax hints:   → wi 4   = wceq 1559   “ cima 5646

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-3an 1099  df-tru 1562  df-fal 1572  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-rab 3414  df-v 3455  df-dif 3905  df-un 3907  df-in 3909  df-ss 3919  df-nul 4284  df-if 4478  df-sn 4580  df-pr 4582  df-op 4586  df-br 5098  df-opab 5160  df-xp 5649  df-cnv 5651  df-dm 5653  df-rn 5654  df-res 5655  df-ima 5656

This theorem is referenced by:  imaeq12d  6046  nfimad  6054  csbima12  6064  elimasni  6076  inisegn0  6083  csbrn  6185  ressn  6267  csbpredg  6289  predprc  6320  fncofn  6633  foima  6778  focnvimacdmdm  6785  f1imacnv  6818  dffv3  6858  fvco2  6959  sspreima  7044  fimacnvinrn2  7048  rescnvimafod  7049  fsn2  7113  funfvima3  7215  isofrlem  7319  isoselem  7320  fnexALT  7927  mptcnfimad  7962  curry1  8077  curry2  8080  fparlem3  8087  fparlem4  8088  suppsnop  8152  ressuppssdif  8159  suppco  8180  imacosupp  8183  naddcllem  8640  eceq1  8712  uniqs2  8752  ecinxp  8768  mapsnd  8862  sbthlem2  9054  sbth  9063  sbthfi  9161  phplem2  9167  php3  9171  marypha1lem  9373  cantnfp1lem3  9629  tcrank  9836  fin4en1  10260  fin1a2lem7  10357  hsmexlem4  10380  hsmexlem5  10381  fpwwe2cbv  10582  fpwwe2lem3  10585  fpwwe2lem12  10594  fpwwecbv  10596  canth4  10599  resunimafz0  14452  limsupgval  15494  isercoll  15686  vdwlem1  17008  vdwlem6  17013  vdwlem7  17014  vdwlem8  17015  vdwlem12  17019  vdwlem13  17020  vdwnn  17025  0ram  17047  ramz2  17051  isacs1i  17680  acsficl  18570  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  efgrelexlema  19780  gsumval3a  19934  gsumval3lem1  19936  gsum2dlem2  20002  gsum2d2  20005  dprddisj  20042  dprdf1o  20065  dprdsn  20069  dprd2dlem2  20073  dprd2dlem1  20074  dprd2da  20075  dprd2db  20076  dmdprdsplit2lem  20078  dpjfval  20088  rngqiprngimf1  21358  frlmup3  21840  islindf  21852  islindf2  21854  lindfind  21856  f1lindf  21862  lmimlbs  21876  coe1mul2lem2  22319  subbascn  23302  cncls2  23321  cncls  23322  cnntr  23323  cnpresti  23336  cnprest  23337  cnt1  23398  cnhaus  23402  cncmp  23440  cnconn  23470  1stcfb  23493  xkoccn  23667  ptrescn  23687  xkococnlem  23707  qtopeu  23764  qtoprest  23765  kqdisj  23780  kqcldsat  23781  ordthmeolem  23849  fmfnfmlem4  24005  ustuqtoplem  24287  utopsnneiplem  24295  utopsnneip  24296  ucncn  24332  metustto  24601  metustexhalf  24604  metustfbas  24605  cfilucfil  24607  metuust  24608  cfilucfil2  24609  metuel  24612  metuel2  24613  psmetutop  24615  restmetu  24618  metucn  24619  pi1addval  25098  iscph  25220  cphsscph  25301  uniioombllem3  25635  dyadmbl  25650  mbfima  25680  mbfimaicc  25681  mbfimasn  25682  ismbfd  25689  ismbf2d  25690  ismbf3d  25704  mbfimaopnlem  25705  i1fd  25731  i1f1  25740  itg11  25741  i1faddlem  25743  i1fmullem  25744  i1fadd  25745  itg1addlem3  25748  itg1mulc  25754  itg2gt0  25810  limcnlp  25928  ellimc3  25929  limcflf  25931  limciun  25944  mdegval  26111  mdeg0  26118  mdegvsca  26124  mdegpropd  26132  deg1val  26144  ig1pval  26224  coeeu  26273  coeeq  26275  pserulm  26473  areambl  27011  cutsval  27861  madeval  27913  addbday  28099  negsval  28106  bdayons  28357  zcuts0  28489  bdaypw2n0bndlem  28544  dfpth2  29886  pthdlem2  29925  cyclnumvtx  29957  eupth2lem3  30395  eupth2  30398  issh  31368  isch  31382  shsval  31472  2ndimaxp  32809  fnpreimac  32833  dfcnv2  32838  mptiffisupp  32856  indsupp  33006  indfsid  33008  s2rnOLD  33083  s3rnOLD  33085  swrdrndisj  33096  pwrssmgc  33139  gsummpt2co  33189  gsumpart  33204  gsumhashmul  33208  cycpmco2rn  33266  qusrn  33556  elrspunidl  33575  rhmimaidl  33579  r1pquslmic  33768  psrbasfsupp  33769  esplyfval  33821  esplyfval0  33822  esplyfval2  33823  vieta  33838  dimval  33859  dimvalfi  33860  ply1degltdimlem  33880  extdgval  33911  algextdeglem3  33977  algextdeglem4  33978  algextdeglem5  33979  smatrcl  34054  locfinreflem  34098  zarclsint  34130  rhmpreimacn  34143  zrhunitpreima  34234  mbfmco2  34523  sibfima  34596  sibfof  34598  eulerpartlemgv  34631  eulerpartlemn  34639  eulerpart  34640  orvcval4  34719  orvcelval  34727  orvcelel  34728  ballotlemscr  34777  fnrelpredd  35348  fineqvr1ombregs  35395  onvfowev  35420  f1resfz0f1d  35425  pthhashvtx  35439  erdszelem3  35504  erdsze  35513  cvmliftlem3  35598  cvmliftlem7  35602  cvmlift2lem9a  35614  msrval  35849  mvtinf  35866  mclsval  35874  mclsax  35880  mthmpps  35893  opelco3  36086  funpartlem  36253  tailval  36694  ptrest  38079  poimirlem1  38081  poimirlem2  38082  poimirlem3  38083  poimirlem4  38084  poimirlem5  38085  poimirlem6  38086  poimirlem7  38087  poimirlem9  38089  poimirlem10  38090  poimirlem11  38091  poimirlem12  38092  poimirlem13  38093  poimirlem14  38094  poimirlem15  38095  poimirlem16  38096  poimirlem17  38097  poimirlem19  38099  poimirlem20  38100  poimirlem22  38102  poimirlem23  38103  poimirlem24  38104  poimirlem25  38105  poimirlem26  38106  poimirlem27  38107  poimirlem28  38108  poimirlem29  38109  poimirlem31  38111  poimirlem32  38112  mblfinlem2  38118  volsupnfl  38125  itg2addnclem2  38132  sstotbnd2  38234  ismtyhmeolem  38264  grpokerinj  38353  lkrfval  39672  aks6d1c6lem5  42755  aks6d1c7lem3  42760  dnnumch3lem  43584  aomclem8  43599  pwfi2f1o  43634  cytpval  43740  frege97d  44289  frege109d  44294  frege131d  44301  nzprmdif  44856  relpfrlem  45490  wessf1ornlem  45724  limsuplesup  46234  limsupvaluz  46243  limsuplt2  46288  limsupge  46296  liminfgval  46297  liminfval2  46303  liminflelimsuplem  46310  liminflelimsup  46311  preimaioomnf  47254  fcoreslem2  47619  f1cof1blem  47629  3f1oss1  47630  afv2co2  47812  imarnf1pr  47837  preimafvelsetpreimafv  47955  imaelsetpreimafv  47962  imasetpreimafvbijlemfo  47972  fundcmpsurbijinjpreimafv  47974  fundcmpsurinj  47976  fundcmpsurbijinj  47977  isgrim  48465  grimuhgr  48470  grimcnv  48471  grimco  48472  uhgrimedgi  48473  isuspgrim0lem  48476  isuspgrim0  48477  upgrimwlklem3  48482  upgrimtrls  48489  upgrimpths  48492  gricushgr  48500  cycldlenngric  48511  isubgrgrim  48512  uhgrimisgrgriclem  48513  clnbgrgrimlem  48516  clnbgrgrim  48517  grimedg  48518  cycl3grtri  48530  isubgr3stgrlem4  48552  uspgrlimlem3  48573  predisj  49393  imasubclem3  49688