Theorem imaeq2d 6015

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

Syntax hints:   → wi 4   = wceq 1540   “ cima 5626

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3397  df-v 3440  df-dif 3908  df-un 3910  df-in 3912  df-ss 3922  df-nul 4287  df-if 4479  df-sn 4580  df-pr 4582  df-op 4586  df-br 5096  df-opab 5158  df-xp 5629  df-cnv 5631  df-dm 5633  df-rn 5634  df-res 5635  df-ima 5636

This theorem is referenced by:  imaeq12d  6016  nfimad  6024  csbima12  6034  elimasni  6046  inisegn0  6053  csbrn  6156  ressn  6237  csbpredg  6259  predprc  6290  fncofn  6603  foima  6745  focnvimacdmdm  6752  f1imacnv  6784  dffv3  6822  fvco2  6924  sspreima  7006  fimacnvinrn2  7010  rescnvimafod  7011  fsn2  7074  funfvima3  7176  isofrlem  7281  isoselem  7282  fnexALT  7893  mptcnfimad  7928  curry1  8044  curry2  8047  fparlem3  8054  fparlem4  8055  suppsnop  8118  ressuppssdif  8125  suppco  8146  imacosupp  8149  naddcllem  8601  eceq1  8671  uniqs2  8711  ecinxp  8726  mapsnd  8820  sbthlem2  9012  sbth  9021  sbthfi  9123  phplem2  9129  php3  9133  marypha1lem  9342  cantnfp1lem3  9595  tcrank  9799  fin4en1  10222  fin1a2lem7  10319  hsmexlem4  10342  hsmexlem5  10343  fpwwe2cbv  10543  fpwwe2lem3  10546  fpwwe2lem12  10555  fpwwecbv  10557  canth4  10560  resunimafz0  14371  limsupgval  15402  isercoll  15594  vdwlem1  16912  vdwlem6  16917  vdwlem7  16918  vdwlem8  16919  vdwlem12  16923  vdwlem13  16924  vdwnn  16929  0ram  16951  ramz2  16955  isacs1i  17582  acsficl  18472  gsumvalx  18569  gsumpropd  18571  gsumpropd2lem  18572  gsumress  18575  efgrelexlema  19647  gsumval3a  19801  gsumval3lem1  19803  gsum2dlem2  19869  gsum2d2  19872  dprddisj  19909  dprdf1o  19932  dprdsn  19936  dprd2dlem2  19940  dprd2dlem1  19941  dprd2da  19942  dprd2db  19943  dmdprdsplit2lem  19945  dpjfval  19955  rngqiprngimf1  21226  frlmup3  21726  islindf  21738  islindf2  21740  lindfind  21742  f1lindf  21748  lmimlbs  21762  coe1mul2lem2  22171  subbascn  23158  cncls2  23177  cncls  23178  cnntr  23179  cnpresti  23192  cnprest  23193  cnt1  23254  cnhaus  23258  cncmp  23296  cnconn  23326  1stcfb  23349  xkoccn  23523  ptrescn  23543  xkococnlem  23563  qtopeu  23620  qtoprest  23621  kqdisj  23636  kqcldsat  23637  ordthmeolem  23705  fmfnfmlem4  23861  ustuqtoplem  24144  utopsnneiplem  24152  utopsnneip  24153  ucncn  24189  metustto  24458  metustexhalf  24461  metustfbas  24462  cfilucfil  24464  metuust  24465  cfilucfil2  24466  metuel  24469  metuel2  24470  psmetutop  24472  restmetu  24475  metucn  24476  pi1addval  24965  iscph  25087  cphsscph  25168  uniioombllem3  25503  dyadmbl  25518  mbfima  25548  mbfimaicc  25549  mbfimasn  25550  ismbfd  25557  ismbf2d  25558  ismbf3d  25572  mbfimaopnlem  25573  i1fd  25599  i1f1  25608  itg11  25609  i1faddlem  25611  i1fmullem  25612  i1fadd  25613  itg1addlem3  25616  itg1mulc  25622  itg2gt0  25678  limcnlp  25796  ellimc3  25797  limcflf  25799  limciun  25812  mdegval  25985  mdeg0  25992  mdegvsca  25998  mdegpropd  26006  deg1val  26018  ig1pval  26098  coeeu  26147  coeeq  26149  pserulm  26348  areambl  26885  scutval  27730  madeval  27781  addsbday  27948  negsval  27955  bdayon  28197  dfpth2  29693  pthdlem2  29732  cyclnumvtx  29764  eupth2lem3  30199  eupth2  30202  issh  31171  isch  31185  shsval  31275  2ndimaxp  32608  fnpreimac  32633  dfcnv2  32638  mptiffisupp  32654  indsupp  32829  s2rnOLD  32904  s3rnOLD  32906  swrdrndisj  32918  pwrssmgc  32961  gsummpt2co  33020  gsumpart  33029  gsumhashmul  33033  cycpmco2rn  33086  qusrn  33365  elrspunidl  33384  rhmimaidl  33388  r1pquslmic  33562  psrbasfsupp  33563  dimval  33586  dimvalfi  33587  ply1degltdimlem  33608  extdgval  33639  algextdeglem3  33705  algextdeglem4  33706  algextdeglem5  33707  smatrcl  33782  locfinreflem  33826  zarclsint  33858  rhmpreimacn  33871  zrhunitpreima  33962  mbfmco2  34252  sibfima  34325  sibfof  34327  eulerpartlemgv  34360  eulerpartlemn  34368  eulerpart  34369  orvcval4  34448  orvcelval  34456  orvcelel  34457  ballotlemscr  34506  fnrelpredd  35075  f1resfz0f1d  35106  pthhashvtx  35120  erdszelem3  35185  erdsze  35194  cvmliftlem3  35279  cvmliftlem7  35283  cvmlift2lem9a  35295  msrval  35530  mvtinf  35547  mclsval  35555  mclsax  35561  mthmpps  35574  opelco3  35767  funpartlem  35935  tailval  36366  ptrest  37618  poimirlem1  37620  poimirlem2  37621  poimirlem3  37622  poimirlem4  37623  poimirlem5  37624  poimirlem6  37625  poimirlem7  37626  poimirlem9  37628  poimirlem10  37629  poimirlem11  37630  poimirlem12  37631  poimirlem13  37632  poimirlem14  37633  poimirlem15  37634  poimirlem16  37635  poimirlem17  37636  poimirlem19  37638  poimirlem20  37639  poimirlem22  37641  poimirlem23  37642  poimirlem24  37643  poimirlem25  37644  poimirlem26  37645  poimirlem27  37646  poimirlem28  37647  poimirlem29  37648  poimirlem31  37650  poimirlem32  37651  mblfinlem2  37657  volsupnfl  37664  itg2addnclem2  37671  sstotbnd2  37773  ismtyhmeolem  37803  grpokerinj  37892  lkrfval  39085  aks6d1c6lem5  42170  aks6d1c7lem3  42175  dnnumch3lem  43039  aomclem8  43054  pwfi2f1o  43089  cytpval  43195  frege97d  43745  frege109d  43750  frege131d  43757  nzprmdif  44312  relpfrlem  44947  wessf1ornlem  45183  limsuplesup  45700  limsupvaluz  45709  limsuplt2  45754  limsupge  45762  liminfgval  45763  liminfval2  45769  liminflelimsuplem  45776  liminflelimsup  45777  preimaioomnf  46720  fcoreslem2  47068  f1cof1blem  47078  3f1oss1  47079  afv2co2  47261  imarnf1pr  47286  preimafvelsetpreimafv  47392  imaelsetpreimafv  47399  imasetpreimafvbijlemfo  47409  fundcmpsurbijinjpreimafv  47411  fundcmpsurinj  47413  fundcmpsurbijinj  47414  isgrim  47886  grimuhgr  47891  grimcnv  47892  grimco  47893  uhgrimedgi  47894  isuspgrim0lem  47897  isuspgrim0  47898  upgrimwlklem3  47903  upgrimtrls  47910  upgrimpths  47913  gricushgr  47921  cycldlenngric  47932  isubgrgrim  47933  uhgrimisgrgriclem  47934  clnbgrgrimlem  47937  clnbgrgrim  47938  grimedg  47939  cycl3grtri  47951  isubgr3stgrlem4  47973  uspgrlimlem3  47994  predisj  48815  imasubclem3  49111