Theorem imaeq2d 6060

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

Syntax hints:   → wi 4   = wceq 1567   “ cima 5662

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-3an 1103  df-tru 1570  df-fal 1580  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-rab 3424  df-v 3465  df-dif 3916  df-un 3918  df-in 3920  df-ss 3930  df-nul 4295  df-if 4490  df-sn 4592  df-pr 4594  df-op 4598  df-br 5111  df-opab 5175  df-xp 5665  df-cnv 5667  df-dm 5669  df-rn 5670  df-res 5671  df-ima 5672

This theorem is referenced by:  imaeq12d  6061  nfimad  6069  csbima12  6079  elimasni  6091  inisegn0  6098  csbrn  6201  ressn  6283  csbpredg  6305  predprc  6336  fncofn  6650  foima  6795  focnvimacdmdm  6802  f1imacnv  6835  dffv3  6875  fvco2  6976  sspreima  7061  fimacnvinrn2  7065  rescnvimafod  7066  fsn2  7130  funfvima3  7232  isofrlem  7336  isoselem  7337  fnexALT  7944  mptcnfimad  7979  curry1  8095  curry2  8098  fparlem3  8105  fparlem4  8106  suppsnop  8170  ressuppssdif  8177  suppco  8198  imacosupp  8201  naddcllem  8658  eceq1  8730  uniqs2  8770  ecinxp  8786  mapsnd  8880  sbthlem2  9072  sbth  9081  sbthfi  9179  phplem2  9185  php3  9189  marypha1lem  9389  cantnfp1lem3  9645  tcrank  9852  fin4en1  10289  fin1a2lem7  10386  hsmexlem4  10409  hsmexlem5  10410  fpwwe2cbv  10611  fpwwe2lem3  10614  fpwwe2lem12  10623  fpwwecbv  10625  canth4  10628  resunimafz0  14478  limsupgval  15523  isercoll  15715  vdwlem1  17037  vdwlem6  17042  vdwlem7  17043  vdwlem8  17044  vdwlem12  17048  vdwlem13  17049  vdwnn  17054  0ram  17076  ramz2  17080  isacs1i  17709  acsficl  18599  gsumvalx  18730  gsumpropd  18732  gsumpropd2lem  18733  gsumress  18736  efgrelexlema  19815  gsumval3a  19969  gsumval3lem1  19971  gsum2dlem2  20037  gsum2d2  20040  dprddisj  20077  dprdf1o  20100  dprdsn  20104  dprd2dlem2  20108  dprd2dlem1  20109  dprd2da  20110  dprd2db  20111  dmdprdsplit2lem  20113  dpjfval  20123  rngqiprngimf1  21407  frlmup3  21915  islindf  21927  islindf2  21929  lindfind  21931  f1lindf  21937  lmimlbs  21951  coe1mul2lem2  22394  subbascn  23376  cncls2  23395  cncls  23396  cnntr  23397  cnpresti  23410  cnprest  23411  cnt1  23472  cnhaus  23476  cncmp  23514  cnconn  23544  1stcfb  23567  xkoccn  23741  ptrescn  23761  xkococnlem  23781  qtopeu  23838  qtoprest  23839  kqdisj  23854  kqcldsat  23855  ordthmeolem  23923  fmfnfmlem4  24079  ustuqtoplem  24361  utopsnneiplem  24369  utopsnneip  24370  ucncn  24406  metustto  24675  metustexhalf  24678  metustfbas  24679  cfilucfil  24681  metuust  24682  cfilucfil2  24683  metuel  24686  metuel2  24687  psmetutop  24689  restmetu  24692  metucn  24693  pi1addval  25172  iscph  25294  cphsscph  25375  uniioombllem3  25709  dyadmbl  25724  mbfima  25754  mbfimaicc  25755  mbfimasn  25756  ismbfd  25763  ismbf2d  25764  ismbf3d  25778  mbfimaopnlem  25779  i1fd  25805  i1f1  25814  itg11  25815  i1faddlem  25817  i1fmullem  25818  i1fadd  25819  itg1addlem3  25822  itg1mulc  25828  itg2gt0  25884  limcnlp  26002  ellimc3  26003  limcflf  26005  limciun  26018  mdegval  26185  mdeg0  26192  mdegvsca  26198  mdegpropd  26206  deg1val  26218  ig1pval  26298  coeeu  26347  coeeq  26349  pserulm  26547  areambl  27085  cutsval  27935  madeval  27987  addbday  28173  negsval  28180  bdayons  28431  zcuts0  28563  bdaypw2n0bndlem  28618  dfpth2  30015  pthdlem2  30054  cyclnumvtx  30086  eupth2lem3  30524  eupth2  30527  issh  31497  isch  31511  shsval  31601  2ndimaxp  32928  fnpreimac  32952  dfcnv2  32957  mptiffisupp  32975  indsupp  33124  indfsid  33126  s2rnOLD  33201  s3rnOLD  33203  swrdrndisj  33214  pwrssmgc  33257  gsummpt2co  33305  gsumpart  33320  gsumhashmul  33324  cycpmco2rn  33382  qusrn  33658  elrspunidl  33676  rhmimaidl  33680  r1pquslmic  33841  psrbasfsupp  33842  esplyfval  33894  esplyfval0  33895  esplyfval2  33896  vieta  33911  dimval  33932  dimvalfi  33933  ply1degltdimlem  33953  extdgval  33984  algextdeglem3  34050  algextdeglem4  34051  algextdeglem5  34052  smatrcl  34127  locfinreflem  34171  zarclsint  34203  rhmpreimacn  34216  zrhunitpreima  34307  mbfmco2  34596  sibfima  34669  sibfof  34671  eulerpartlemgv  34704  eulerpartlemn  34712  eulerpart  34713  orvcval4  34792  orvcelval  34800  orvcelel  34801  ballotlemscr  34850  fnrelpredd  35421  fineqvr1ombregs  35470  onvfowev  35495  f1resfz0f1d  35500  pthhashvtx  35515  erdszelem3  35580  erdsze  35589  cvmliftlem3  35674  cvmliftlem7  35678  cvmlift2lem9a  35690  msrval  35925  mvtinf  35942  mclsval  35950  mclsax  35956  mthmpps  35969  opelco3  36162  funpartlem  36329  tailval  36769  ptrest  38153  poimirlem1  38155  poimirlem2  38156  poimirlem3  38157  poimirlem4  38158  poimirlem5  38159  poimirlem6  38160  poimirlem7  38161  poimirlem9  38163  poimirlem10  38164  poimirlem11  38165  poimirlem12  38166  poimirlem13  38167  poimirlem14  38168  poimirlem15  38169  poimirlem16  38170  poimirlem17  38171  poimirlem19  38173  poimirlem20  38174  poimirlem22  38176  poimirlem23  38177  poimirlem24  38178  poimirlem25  38179  poimirlem26  38180  poimirlem27  38181  poimirlem28  38182  poimirlem29  38183  poimirlem31  38185  poimirlem32  38186  mblfinlem2  38192  volsupnfl  38199  itg2addnclem2  38206  sstotbnd2  38308  ismtyhmeolem  38338  grpokerinj  38427  lkrfval  39746  aks6d1c6lem5  42829  aks6d1c7lem3  42834  dnnumch3lem  43658  aomclem8  43673  pwfi2f1o  43708  cytpval  43814  frege97d  44363  frege109d  44368  frege131d  44375  nzprmdif  44914  relpfrlem  45547  wessf1ornlem  45788  limsuplesup  46298  limsupvaluz  46307  limsuplt2  46352  limsupge  46360  liminfgval  46361  liminfval2  46367  liminflelimsuplem  46374  liminflelimsup  46375  preimaioomnf  47318  fcoreslem2  47683  f1cof1blem  47693  3f1oss1  47694  afv2co2  47876  imarnf1pr  47901  preimafvelsetpreimafv  48019  imaelsetpreimafv  48026  imasetpreimafvbijlemfo  48036  fundcmpsurbijinjpreimafv  48038  fundcmpsurinj  48040  fundcmpsurbijinj  48041  isgrim  48529  grimuhgr  48534  grimcnv  48535  grimco  48536  uhgrimedgi  48537  isuspgrim0lem  48540  isuspgrim0  48541  upgrimwlklem3  48546  upgrimtrls  48553  upgrimpths  48556  gricushgr  48564  cycldlenngric  48575  isubgrgrim  48576  uhgrimisgrgriclem  48577  clnbgrgrimlem  48580  clnbgrgrim  48581  grimedg  48582  cycl3grtri  48594  isubgr3stgrlem4  48616  uspgrlimlem3  48637  predisj  49467  imasubclem3  49762