Theorem imaeq2d 6027

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

Syntax hints:   → wi 4   = wceq 1542   “ cima 5635

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-3an 1089  df-tru 1545  df-fal 1555  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-rab 3402  df-v 3444  df-dif 3906  df-un 3908  df-in 3910  df-ss 3920  df-nul 4288  df-if 4482  df-sn 4583  df-pr 4585  df-op 4589  df-br 5101  df-opab 5163  df-xp 5638  df-cnv 5640  df-dm 5642  df-rn 5643  df-res 5644  df-ima 5645

This theorem is referenced by:  imaeq12d  6028  nfimad  6036  csbima12  6046  elimasni  6058  inisegn0  6065  csbrn  6169  ressn  6251  csbpredg  6273  predprc  6304  fncofn  6617  foima  6759  focnvimacdmdm  6766  f1imacnv  6798  dffv3  6838  fvco2  6939  sspreima  7022  fimacnvinrn2  7026  rescnvimafod  7027  fsn2  7091  funfvima3  7192  isofrlem  7296  isoselem  7297  fnexALT  7905  mptcnfimad  7940  curry1  8056  curry2  8059  fparlem3  8066  fparlem4  8067  suppsnop  8130  ressuppssdif  8137  suppco  8158  imacosupp  8161  naddcllem  8614  eceq1  8685  uniqs2  8725  ecinxp  8741  mapsnd  8836  sbthlem2  9028  sbth  9037  sbthfi  9135  phplem2  9141  php3  9145  marypha1lem  9348  cantnfp1lem3  9601  tcrank  9808  fin4en1  10231  fin1a2lem7  10328  hsmexlem4  10351  hsmexlem5  10352  fpwwe2cbv  10553  fpwwe2lem3  10556  fpwwe2lem12  10565  fpwwecbv  10567  canth4  10570  resunimafz0  14380  limsupgval  15411  isercoll  15603  vdwlem1  16921  vdwlem6  16926  vdwlem7  16927  vdwlem8  16928  vdwlem12  16932  vdwlem13  16933  vdwnn  16938  0ram  16960  ramz2  16964  isacs1i  17592  acsficl  18482  gsumvalx  18613  gsumpropd  18615  gsumpropd2lem  18616  gsumress  18619  efgrelexlema  19690  gsumval3a  19844  gsumval3lem1  19846  gsum2dlem2  19912  gsum2d2  19915  dprddisj  19952  dprdf1o  19975  dprdsn  19979  dprd2dlem2  19983  dprd2dlem1  19984  dprd2da  19985  dprd2db  19986  dmdprdsplit2lem  19988  dpjfval  19998  rngqiprngimf1  21267  frlmup3  21767  islindf  21779  islindf2  21781  lindfind  21783  f1lindf  21789  lmimlbs  21803  coe1mul2lem2  22222  subbascn  23210  cncls2  23229  cncls  23230  cnntr  23231  cnpresti  23244  cnprest  23245  cnt1  23306  cnhaus  23310  cncmp  23348  cnconn  23378  1stcfb  23401  xkoccn  23575  ptrescn  23595  xkococnlem  23615  qtopeu  23672  qtoprest  23673  kqdisj  23688  kqcldsat  23689  ordthmeolem  23757  fmfnfmlem4  23913  ustuqtoplem  24195  utopsnneiplem  24203  utopsnneip  24204  ucncn  24240  metustto  24509  metustexhalf  24512  metustfbas  24513  cfilucfil  24515  metuust  24516  cfilucfil2  24517  metuel  24520  metuel2  24521  psmetutop  24523  restmetu  24526  metucn  24527  pi1addval  25016  iscph  25138  cphsscph  25219  uniioombllem3  25554  dyadmbl  25569  mbfima  25599  mbfimaicc  25600  mbfimasn  25601  ismbfd  25608  ismbf2d  25609  ismbf3d  25623  mbfimaopnlem  25624  i1fd  25650  i1f1  25659  itg11  25660  i1faddlem  25662  i1fmullem  25663  i1fadd  25664  itg1addlem3  25667  itg1mulc  25673  itg2gt0  25729  limcnlp  25847  ellimc3  25848  limcflf  25850  limciun  25863  mdegval  26036  mdeg0  26043  mdegvsca  26049  mdegpropd  26057  deg1val  26069  ig1pval  26149  coeeu  26198  coeeq  26200  pserulm  26399  areambl  26936  cutsval  27788  madeval  27840  addbday  28026  negsval  28033  bdayons  28284  zcuts0  28416  bdaypw2n0bndlem  28471  dfpth2  29814  pthdlem2  29853  cyclnumvtx  29885  eupth2lem3  30323  eupth2  30326  issh  31295  isch  31309  shsval  31399  2ndimaxp  32735  fnpreimac  32759  dfcnv2  32764  mptiffisupp  32782  indsupp  32959  indfsid  32961  s2rnOLD  33036  s3rnOLD  33038  swrdrndisj  33049  pwrssmgc  33092  gsummpt2co  33141  gsumpart  33156  gsumhashmul  33160  cycpmco2rn  33218  qusrn  33501  elrspunidl  33520  rhmimaidl  33524  r1pquslmic  33703  psrbasfsupp  33704  esplyfval  33739  esplyfval0  33740  esplyfval2  33741  vieta  33756  dimval  33777  dimvalfi  33778  ply1degltdimlem  33799  extdgval  33830  algextdeglem3  33896  algextdeglem4  33897  algextdeglem5  33898  smatrcl  33973  locfinreflem  34017  zarclsint  34049  rhmpreimacn  34062  zrhunitpreima  34153  mbfmco2  34442  sibfima  34515  sibfof  34517  eulerpartlemgv  34550  eulerpartlemn  34558  eulerpart  34559  orvcval4  34638  orvcelval  34646  orvcelel  34647  ballotlemscr  34696  fnrelpredd  35266  fineqvr1ombregs  35313  f1resfz0f1d  35327  pthhashvtx  35341  erdszelem3  35406  erdsze  35415  cvmliftlem3  35500  cvmliftlem7  35504  cvmlift2lem9a  35516  msrval  35751  mvtinf  35768  mclsval  35776  mclsax  35782  mthmpps  35795  opelco3  35988  funpartlem  36155  tailval  36586  ptrest  37867  poimirlem1  37869  poimirlem2  37870  poimirlem3  37871  poimirlem4  37872  poimirlem5  37873  poimirlem6  37874  poimirlem7  37875  poimirlem9  37877  poimirlem10  37878  poimirlem11  37879  poimirlem12  37880  poimirlem13  37881  poimirlem14  37882  poimirlem15  37883  poimirlem16  37884  poimirlem17  37885  poimirlem19  37887  poimirlem20  37888  poimirlem22  37890  poimirlem23  37891  poimirlem24  37892  poimirlem25  37893  poimirlem26  37894  poimirlem27  37895  poimirlem28  37896  poimirlem29  37897  poimirlem31  37899  poimirlem32  37900  mblfinlem2  37906  volsupnfl  37913  itg2addnclem2  37920  sstotbnd2  38022  ismtyhmeolem  38052  grpokerinj  38141  lkrfval  39460  aks6d1c6lem5  42544  aks6d1c7lem3  42549  dnnumch3lem  43400  aomclem8  43415  pwfi2f1o  43450  cytpval  43556  frege97d  44105  frege109d  44110  frege131d  44117  nzprmdif  44672  relpfrlem  45306  wessf1ornlem  45541  limsuplesup  46054  limsupvaluz  46063  limsuplt2  46108  limsupge  46116  liminfgval  46117  liminfval2  46123  liminflelimsuplem  46130  liminflelimsup  46131  preimaioomnf  47074  fcoreslem2  47421  f1cof1blem  47431  3f1oss1  47432  afv2co2  47614  imarnf1pr  47639  preimafvelsetpreimafv  47745  imaelsetpreimafv  47752  imasetpreimafvbijlemfo  47762  fundcmpsurbijinjpreimafv  47764  fundcmpsurinj  47766  fundcmpsurbijinj  47767  isgrim  48239  grimuhgr  48244  grimcnv  48245  grimco  48246  uhgrimedgi  48247  isuspgrim0lem  48250  isuspgrim0  48251  upgrimwlklem3  48256  upgrimtrls  48263  upgrimpths  48266  gricushgr  48274  cycldlenngric  48285  isubgrgrim  48286  uhgrimisgrgriclem  48287  clnbgrgrimlem  48290  clnbgrgrim  48291  grimedg  48292  cycl3grtri  48304  isubgr3stgrlem4  48326  uspgrlimlem3  48347  predisj  49167  imasubclem3  49462