Theorem imaeq2d 6079

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

Syntax hints:   → wi 4   = wceq 1536   “ cima 5691

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-rab 3433  df-v 3479  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-nul 4339  df-if 4531  df-sn 4631  df-pr 4633  df-op 4637  df-br 5148  df-opab 5210  df-xp 5694  df-cnv 5696  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701

This theorem is referenced by:  imaeq12d  6080  nfimad  6088  csbima12  6098  elimasngOLD  6110  elimasni  6111  inisegn0  6118  csbrn  6224  ressn  6306  csbpredg  6328  predprc  6360  fncofn  6685  foima  6825  focnvimacdmdm  6832  f1imacnv  6864  dffv3  6902  fvco2  7005  sspreima  7087  fimacnvinrn2  7091  rescnvimafod  7092  fsn2  7155  funfvima3  7255  isofrlem  7359  isoselem  7360  fnexALT  7973  mptcnfimad  8009  curry1  8127  curry2  8130  fparlem3  8137  fparlem4  8138  suppsnop  8201  ressuppssdif  8208  suppco  8229  imacosupp  8232  naddcllem  8712  eceq1  8782  uniqs2  8817  ecinxp  8830  mapsnd  8924  sbthlem2  9122  sbth  9131  sbthfi  9236  phplem2  9242  php3  9246  phplem4OLD  9254  php3OLD  9258  marypha1lem  9470  cantnfp1lem3  9717  tcrank  9921  fin4en1  10346  fin1a2lem7  10443  hsmexlem4  10466  hsmexlem5  10467  fpwwe2cbv  10667  fpwwe2lem3  10670  fpwwe2lem12  10679  fpwwecbv  10681  canth4  10684  resunimafz0  14480  limsupgval  15508  isercoll  15700  vdwlem1  17014  vdwlem6  17019  vdwlem7  17020  vdwlem8  17021  vdwlem12  17025  vdwlem13  17026  vdwnn  17031  0ram  17053  ramz2  17057  isacs1i  17701  acsficl  18604  gsumvalx  18701  gsumpropd  18703  gsumpropd2lem  18704  gsumress  18707  efgrelexlema  19781  gsumval3a  19935  gsumval3lem1  19937  gsum2dlem2  20003  gsum2d2  20006  dprddisj  20043  dprdf1o  20066  dprdsn  20070  dprd2dlem2  20074  dprd2dlem1  20075  dprd2da  20076  dprd2db  20077  dmdprdsplit2lem  20079  dpjfval  20089  rngqiprngimf1  21327  frlmup3  21837  islindf  21849  islindf2  21851  lindfind  21853  f1lindf  21859  lmimlbs  21873  coe1mul2lem2  22286  subbascn  23277  cncls2  23296  cncls  23297  cnntr  23298  cnpresti  23311  cnprest  23312  cnt1  23373  cnhaus  23377  cncmp  23415  cnconn  23445  1stcfb  23468  xkoccn  23642  ptrescn  23662  xkococnlem  23682  qtopeu  23739  qtoprest  23740  kqdisj  23755  kqcldsat  23756  ordthmeolem  23824  fmfnfmlem4  23980  ustuqtoplem  24263  utopsnneiplem  24271  utopsnneip  24272  ucncn  24309  metustto  24581  metustexhalf  24584  metustfbas  24585  cfilucfil  24587  metuust  24588  cfilucfil2  24589  metuel  24592  metuel2  24593  psmetutop  24595  restmetu  24598  metucn  24599  pi1addval  25094  iscph  25217  cphsscph  25298  uniioombllem3  25633  dyadmbl  25648  mbfima  25678  mbfimaicc  25679  mbfimasn  25680  ismbfd  25687  ismbf2d  25688  ismbf3d  25702  mbfimaopnlem  25703  i1fd  25729  i1f1  25738  itg11  25739  i1faddlem  25741  i1fmullem  25742  i1fadd  25743  itg1addlem3  25746  itg1mulc  25753  itg2gt0  25809  limcnlp  25927  ellimc3  25928  limcflf  25930  limciun  25943  mdegval  26116  mdeg0  26123  mdegvsca  26129  mdegpropd  26137  deg1val  26149  ig1pval  26229  coeeu  26278  coeeq  26280  pserulm  26479  areambl  27015  scutval  27859  madeval  27905  addsbday  28064  negsval  28071  pthdlem2  29800  eupth2lem3  30264  eupth2  30267  issh  31236  isch  31250  shsval  31340  2ndimaxp  32662  fnpreimac  32687  dfcnv2  32692  mptiffisupp  32707  s2rnOLD  32912  s3rnOLD  32914  swrdrndisj  32926  pwrssmgc  32974  gsummpt2co  33033  gsumpart  33042  gsumhashmul  33046  cycpmco2rn  33127  qusrn  33416  elrspunidl  33435  rhmimaidl  33439  r1pquslmic  33610  dimval  33627  dimvalfi  33628  ply1degltdimlem  33649  extdgval  33681  algextdeglem3  33724  algextdeglem4  33725  algextdeglem5  33726  smatrcl  33756  locfinreflem  33800  zarclsint  33832  rhmpreimacn  33845  zrhunitpreima  33938  mbfmco2  34246  sibfima  34319  sibfof  34321  eulerpartlemgv  34354  eulerpartlemn  34362  eulerpart  34363  orvcval4  34441  orvcelval  34449  orvcelel  34450  ballotlemscr  34499  fnrelpredd  35081  f1resfz0f1d  35097  pthhashvtx  35111  erdszelem3  35177  erdsze  35186  cvmliftlem3  35271  cvmliftlem7  35275  cvmlift2lem9a  35287  msrval  35522  mvtinf  35539  mclsval  35547  mclsax  35553  mthmpps  35566  opelco3  35755  funpartlem  35923  tailval  36355  ptrest  37605  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem5  37611  poimirlem6  37612  poimirlem7  37613  poimirlem9  37615  poimirlem10  37616  poimirlem11  37617  poimirlem12  37618  poimirlem13  37619  poimirlem14  37620  poimirlem15  37621  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem22  37628  poimirlem23  37629  poimirlem24  37630  poimirlem25  37631  poimirlem26  37632  poimirlem27  37633  poimirlem28  37634  poimirlem29  37635  poimirlem31  37637  poimirlem32  37638  mblfinlem2  37644  volsupnfl  37651  itg2addnclem2  37658  sstotbnd2  37760  ismtyhmeolem  37790  grpokerinj  37879  lkrfval  39068  aks6d1c6lem5  42158  aks6d1c7lem3  42163  dnnumch3lem  43034  aomclem8  43049  pwfi2f1o  43084  cytpval  43190  frege97d  43741  frege109d  43746  frege131d  43753  nzprmdif  44314  wessf1ornlem  45127  limsuplesup  45654  limsupvaluz  45663  limsuplt2  45708  limsupge  45716  liminfgval  45717  liminfval2  45723  liminflelimsuplem  45730  liminflelimsup  45731  preimaioomnf  46674  fcoreslem2  47013  f1cof1blem  47023  3f1oss1  47024  afv2co2  47206  imarnf1pr  47231  preimafvelsetpreimafv  47312  imaelsetpreimafv  47319  imasetpreimafvbijlemfo  47329  fundcmpsurbijinjpreimafv  47331  fundcmpsurinj  47333  fundcmpsurbijinj  47334  isgrim  47805  isuspgrim0lem  47808  isuspgrim0  47809  grimuhgr  47815  grimcnv  47816  grimco  47817  gricushgr  47823  isubgrgrim  47834  uhgrimisgrgriclem  47835  clnbgrgrimlem  47838  clnbgrgrim  47839  grimedg  47840  isubgr3stgrlem4  47871  uspgrlimlem3  47892  predisj  48658