Theorem imaeq2d 6004

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

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

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 2113  ax-9 2121  ax-ext 2703

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 2710  df-cleq 2723  df-clel 2806  df-rab 3396  df-v 3438  df-dif 3900  df-un 3902  df-in 3904  df-ss 3914  df-nul 4279  df-if 4471  df-sn 4572  df-pr 4574  df-op 4578  df-br 5087  df-opab 5149  df-xp 5617  df-cnv 5619  df-dm 5621  df-rn 5622  df-res 5623  df-ima 5624

This theorem is referenced by:  imaeq12d  6005  nfimad  6013  csbima12  6023  elimasni  6035  inisegn0  6042  csbrn  6145  ressn  6227  csbpredg  6249  predprc  6280  fncofn  6593  foima  6735  focnvimacdmdm  6742  f1imacnv  6774  dffv3  6813  fvco2  6914  sspreima  6996  fimacnvinrn2  7000  rescnvimafod  7001  fsn2  7064  funfvima3  7165  isofrlem  7269  isoselem  7270  fnexALT  7878  mptcnfimad  7913  curry1  8029  curry2  8032  fparlem3  8039  fparlem4  8040  suppsnop  8103  ressuppssdif  8110  suppco  8131  imacosupp  8134  naddcllem  8586  eceq1  8656  uniqs2  8696  ecinxp  8711  mapsnd  8805  sbthlem2  8996  sbth  9005  sbthfi  9103  phplem2  9109  php3  9113  marypha1lem  9312  cantnfp1lem3  9565  tcrank  9772  fin4en1  10195  fin1a2lem7  10292  hsmexlem4  10315  hsmexlem5  10316  fpwwe2cbv  10516  fpwwe2lem3  10519  fpwwe2lem12  10528  fpwwecbv  10530  canth4  10533  resunimafz0  14347  limsupgval  15378  isercoll  15570  vdwlem1  16888  vdwlem6  16893  vdwlem7  16894  vdwlem8  16895  vdwlem12  16899  vdwlem13  16900  vdwnn  16905  0ram  16927  ramz2  16931  isacs1i  17558  acsficl  18448  gsumvalx  18579  gsumpropd  18581  gsumpropd2lem  18582  gsumress  18585  efgrelexlema  19656  gsumval3a  19810  gsumval3lem1  19812  gsum2dlem2  19878  gsum2d2  19881  dprddisj  19918  dprdf1o  19941  dprdsn  19945  dprd2dlem2  19949  dprd2dlem1  19950  dprd2da  19951  dprd2db  19952  dmdprdsplit2lem  19954  dpjfval  19964  rngqiprngimf1  21232  frlmup3  21732  islindf  21744  islindf2  21746  lindfind  21748  f1lindf  21754  lmimlbs  21768  coe1mul2lem2  22177  subbascn  23164  cncls2  23183  cncls  23184  cnntr  23185  cnpresti  23198  cnprest  23199  cnt1  23260  cnhaus  23264  cncmp  23302  cnconn  23332  1stcfb  23355  xkoccn  23529  ptrescn  23549  xkococnlem  23569  qtopeu  23626  qtoprest  23627  kqdisj  23642  kqcldsat  23643  ordthmeolem  23711  fmfnfmlem4  23867  ustuqtoplem  24149  utopsnneiplem  24157  utopsnneip  24158  ucncn  24194  metustto  24463  metustexhalf  24466  metustfbas  24467  cfilucfil  24469  metuust  24470  cfilucfil2  24471  metuel  24474  metuel2  24475  psmetutop  24477  restmetu  24480  metucn  24481  pi1addval  24970  iscph  25092  cphsscph  25173  uniioombllem3  25508  dyadmbl  25523  mbfima  25553  mbfimaicc  25554  mbfimasn  25555  ismbfd  25562  ismbf2d  25563  ismbf3d  25577  mbfimaopnlem  25578  i1fd  25604  i1f1  25613  itg11  25614  i1faddlem  25616  i1fmullem  25617  i1fadd  25618  itg1addlem3  25621  itg1mulc  25627  itg2gt0  25683  limcnlp  25801  ellimc3  25802  limcflf  25804  limciun  25817  mdegval  25990  mdeg0  25997  mdegvsca  26003  mdegpropd  26011  deg1val  26023  ig1pval  26103  coeeu  26152  coeeq  26154  pserulm  26353  areambl  26890  scutval  27736  madeval  27788  addsbday  27955  negsval  27962  bdayon  28204  dfpth2  29702  pthdlem2  29741  cyclnumvtx  29773  eupth2lem3  30208  eupth2  30211  issh  31180  isch  31194  shsval  31284  2ndimaxp  32620  fnpreimac  32645  dfcnv2  32650  mptiffisupp  32666  indsupp  32840  indfsid  32842  s2rnOLD  32917  s3rnOLD  32919  swrdrndisj  32930  pwrssmgc  32973  gsummpt2co  33020  gsumpart  33029  gsumhashmul  33033  cycpmco2rn  33086  qusrn  33366  elrspunidl  33385  rhmimaidl  33389  r1pquslmic  33563  psrbasfsupp  33564  esplyfval  33578  dimval  33605  dimvalfi  33606  ply1degltdimlem  33627  extdgval  33658  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  smatrcl  33801  locfinreflem  33845  zarclsint  33877  rhmpreimacn  33890  zrhunitpreima  33981  mbfmco2  34270  sibfima  34343  sibfof  34345  eulerpartlemgv  34378  eulerpartlemn  34386  eulerpart  34387  orvcval4  34466  orvcelval  34474  orvcelel  34475  ballotlemscr  34524  fnrelpredd  35094  fineqvr1ombregs  35127  f1resfz0f1d  35150  pthhashvtx  35164  erdszelem3  35229  erdsze  35238  cvmliftlem3  35323  cvmliftlem7  35327  cvmlift2lem9a  35339  msrval  35574  mvtinf  35591  mclsval  35599  mclsax  35605  mthmpps  35618  opelco3  35811  funpartlem  35976  tailval  36407  ptrest  37659  poimirlem1  37661  poimirlem2  37662  poimirlem3  37663  poimirlem4  37664  poimirlem5  37665  poimirlem6  37666  poimirlem7  37667  poimirlem9  37669  poimirlem10  37670  poimirlem11  37671  poimirlem12  37672  poimirlem13  37673  poimirlem14  37674  poimirlem15  37675  poimirlem16  37676  poimirlem17  37677  poimirlem19  37679  poimirlem20  37680  poimirlem22  37682  poimirlem23  37683  poimirlem24  37684  poimirlem25  37685  poimirlem26  37686  poimirlem27  37687  poimirlem28  37688  poimirlem29  37689  poimirlem31  37691  poimirlem32  37692  mblfinlem2  37698  volsupnfl  37705  itg2addnclem2  37712  sstotbnd2  37814  ismtyhmeolem  37844  grpokerinj  37933  lkrfval  39126  aks6d1c6lem5  42210  aks6d1c7lem3  42215  dnnumch3lem  43079  aomclem8  43094  pwfi2f1o  43129  cytpval  43235  frege97d  43785  frege109d  43790  frege131d  43797  nzprmdif  44352  relpfrlem  44986  wessf1ornlem  45222  limsuplesup  45737  limsupvaluz  45746  limsuplt2  45791  limsupge  45799  liminfgval  45800  liminfval2  45806  liminflelimsuplem  45813  liminflelimsup  45814  preimaioomnf  46757  fcoreslem2  47095  f1cof1blem  47105  3f1oss1  47106  afv2co2  47288  imarnf1pr  47313  preimafvelsetpreimafv  47419  imaelsetpreimafv  47426  imasetpreimafvbijlemfo  47436  fundcmpsurbijinjpreimafv  47438  fundcmpsurinj  47440  fundcmpsurbijinj  47441  isgrim  47913  grimuhgr  47918  grimcnv  47919  grimco  47920  uhgrimedgi  47921  isuspgrim0lem  47924  isuspgrim0  47925  upgrimwlklem3  47930  upgrimtrls  47937  upgrimpths  47940  gricushgr  47948  cycldlenngric  47959  isubgrgrim  47960  uhgrimisgrgriclem  47961  clnbgrgrimlem  47964  clnbgrgrim  47965  grimedg  47966  cycl3grtri  47978  isubgr3stgrlem4  48000  uspgrlimlem3  48021  predisj  48842  imasubclem3  49138