Theorem imaeq2d 6057

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

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

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 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-3an 1089  df-tru 1544  df-fal 1554  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-rab 3433  df-v 3476  df-dif 3950  df-un 3952  df-in 3954  df-ss 3964  df-nul 4322  df-if 4528  df-sn 4628  df-pr 4630  df-op 4634  df-br 5148  df-opab 5210  df-xp 5681  df-cnv 5683  df-dm 5685  df-rn 5686  df-res 5687  df-ima 5688

This theorem is referenced by:  imaeq12d  6058  nfimad  6066  csbima12  6075  elimasngOLD  6086  elimasni  6087  inisegn0  6094  csbrn  6199  ressn  6281  csbpredg  6303  predprc  6336  fncofn  6663  foima  6807  focnvimacdmdm  6814  f1imacnv  6846  dffv3  6884  fvco2  6985  sspreima  7066  fimacnvinrn2  7071  rescnvimafod  7072  fsn2  7130  funfvima3  7234  isofrlem  7333  isoselem  7334  fnexALT  7933  curry1  8086  curry2  8089  fparlem3  8096  fparlem4  8097  suppsnop  8159  ressuppssdif  8166  suppco  8187  imacosupp  8190  naddcllem  8671  eceq1  8737  uniqs2  8769  ecinxp  8782  mapsnd  8876  sbthlem2  9080  sbth  9089  sbthfi  9198  phplem2  9204  php3  9208  phplem4OLD  9216  php3OLD  9220  marypha1lem  9424  cantnfp1lem3  9671  tcrank  9875  fin4en1  10300  fin1a2lem7  10397  hsmexlem4  10420  hsmexlem5  10421  fpwwe2cbv  10621  fpwwe2lem3  10624  fpwwe2lem12  10633  fpwwecbv  10635  canth4  10638  resunimafz0  14400  limsupgval  15416  isercoll  15610  vdwlem1  16910  vdwlem6  16915  vdwlem7  16916  vdwlem8  16917  vdwlem12  16921  vdwlem13  16922  vdwnn  16927  0ram  16949  ramz2  16953  isacs1i  17597  acsficl  18496  gsumvalx  18591  gsumpropd  18593  gsumpropd2lem  18594  gsumress  18597  efgrelexlema  19611  gsumval3a  19765  gsumval3lem1  19767  gsum2dlem2  19833  gsum2d2  19836  dprddisj  19873  dprdf1o  19896  dprdsn  19900  dprd2dlem2  19904  dprd2dlem1  19905  dprd2da  19906  dprd2db  19907  dmdprdsplit2lem  19909  dpjfval  19919  frlmup3  21346  islindf  21358  islindf2  21360  lindfind  21362  f1lindf  21368  lmimlbs  21382  coe1mul2lem2  21781  subbascn  22749  cncls2  22768  cncls  22769  cnntr  22770  cnpresti  22783  cnprest  22784  cnt1  22845  cnhaus  22849  cncmp  22887  cnconn  22917  1stcfb  22940  xkoccn  23114  ptrescn  23134  xkococnlem  23154  qtopeu  23211  qtoprest  23212  kqdisj  23227  kqcldsat  23228  ordthmeolem  23296  fmfnfmlem4  23452  ustuqtoplem  23735  utopsnneiplem  23743  utopsnneip  23744  ucncn  23781  metustto  24053  metustexhalf  24056  metustfbas  24057  cfilucfil  24059  metuust  24060  cfilucfil2  24061  metuel  24064  metuel2  24065  psmetutop  24067  restmetu  24070  metucn  24071  pi1addval  24555  iscph  24678  cphsscph  24759  uniioombllem3  25093  dyadmbl  25108  mbfima  25138  mbfimaicc  25139  mbfimasn  25140  ismbfd  25147  ismbf2d  25148  ismbf3d  25162  mbfimaopnlem  25163  i1fd  25189  i1f1  25198  itg11  25199  i1faddlem  25201  i1fmullem  25202  i1fadd  25203  itg1addlem3  25206  itg1mulc  25213  itg2gt0  25269  limcnlp  25386  ellimc3  25387  limcflf  25389  limciun  25402  mdegval  25572  mdeg0  25579  mdegvsca  25585  mdegpropd  25593  deg1val  25605  ig1pval  25681  coeeu  25730  coeeq  25732  pserulm  25925  areambl  26452  scutval  27290  madeval  27336  negsval  27489  pthdlem2  29014  eupth2lem3  29478  eupth2  29481  issh  30448  isch  30462  shsval  30552  2ndimaxp  31859  fnpreimac  31883  dfcnv2  31888  mptiffisupp  31902  s2rn  32097  s3rn  32099  swrdrndisj  32108  pwrssmgc  32157  gsummpt2co  32187  gsumpart  32194  gsumhashmul  32195  cycpmco2rn  32271  qusrn  32508  elrspunidl  32534  rhmimaidl  32538  dimval  32674  dimvalfi  32675  ply1degltdimlem  32695  extdgval  32721  algextdeglem1  32760  smatrcl  32764  locfinreflem  32808  zarclsint  32840  rhmpreimacn  32853  zrhunitpreima  32946  mbfmco2  33252  sibfima  33325  sibfof  33327  eulerpartlemgv  33360  eulerpartlemn  33368  eulerpart  33369  orvcval4  33447  orvcelval  33455  orvcelel  33456  ballotlemscr  33505  fnrelpredd  34080  f1resfz0f1d  34091  pthhashvtx  34106  erdszelem3  34172  erdsze  34181  cvmliftlem3  34266  cvmliftlem7  34270  cvmlift2lem9a  34282  msrval  34517  mvtinf  34534  mclsval  34542  mclsax  34548  mthmpps  34561  opelco3  34734  funpartlem  34902  tailval  35246  ptrest  36475  poimirlem1  36477  poimirlem2  36478  poimirlem3  36479  poimirlem4  36480  poimirlem5  36481  poimirlem6  36482  poimirlem7  36483  poimirlem9  36485  poimirlem10  36486  poimirlem11  36487  poimirlem12  36488  poimirlem13  36489  poimirlem14  36490  poimirlem15  36491  poimirlem16  36492  poimirlem17  36493  poimirlem19  36495  poimirlem20  36496  poimirlem22  36498  poimirlem23  36499  poimirlem24  36500  poimirlem25  36501  poimirlem26  36502  poimirlem27  36503  poimirlem28  36504  poimirlem29  36505  poimirlem31  36507  poimirlem32  36508  mblfinlem2  36514  volsupnfl  36521  itg2addnclem2  36528  sstotbnd2  36630  ismtyhmeolem  36660  grpokerinj  36749  lkrfval  37945  dnnumch3lem  41773  aomclem8  41788  pwfi2f1o  41823  cytpval  41936  frege97d  42488  frege109d  42493  frege131d  42500  nzprmdif  43063  wessf1ornlem  43867  limsuplesup  44401  limsupvaluz  44410  limsuplt2  44455  limsupge  44463  liminfgval  44464  liminfval2  44470  liminflelimsuplem  44477  liminflelimsup  44478  preimaioomnf  45421  fcoreslem2  45760  f1cof1blem  45770  afv2co2  45951  imarnf1pr  45976  preimafvelsetpreimafv  46042  imaelsetpreimafv  46049  imasetpreimafvbijlemfo  46059  fundcmpsurbijinjpreimafv  46061  fundcmpsurinj  46063  fundcmpsurbijinj  46064  isomgr  46477  isomushgr  46480  isomgrsym  46490  isomgrtrlem  46492  rngqiprngimf1  46765  predisj  47448