Theorem imaeq2d 6012

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

Syntax hints:   → wi 4   = wceq 1547   “ cima 5621

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-3an 1094  df-tru 1550  df-fal 1560  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-rab 3392  df-v 3433  df-dif 3886  df-un 3888  df-in 3890  df-ss 3900  df-nul 4262  df-if 4455  df-sn 4556  df-pr 4558  df-op 4562  df-br 5073  df-opab 5135  df-xp 5624  df-cnv 5626  df-dm 5628  df-rn 5629  df-res 5630  df-ima 5631

This theorem is referenced by:  imaeq12d  6013  nfimad  6021  csbima12  6031  elimasni  6043  inisegn0  6050  csbrn  6154  ressn  6236  csbpredg  6258  predprc  6289  fncofn  6602  foima  6744  focnvimacdmdm  6751  f1imacnv  6783  dffv3  6823  fvco2  6924  sspreima  7009  fimacnvinrn2  7013  rescnvimafod  7014  fsn2  7078  funfvima3  7180  isofrlem  7284  isoselem  7285  fnexALT  7893  mptcnfimad  7928  curry1  8043  curry2  8046  fparlem3  8053  fparlem4  8054  suppsnop  8118  ressuppssdif  8125  suppco  8146  imacosupp  8149  naddcllem  8602  eceq1  8673  uniqs2  8713  ecinxp  8729  mapsnd  8824  sbthlem2  9016  sbth  9025  sbthfi  9123  phplem2  9129  php3  9133  marypha1lem  9336  cantnfp1lem3  9592  tcrank  9799  fin4en1  10222  fin1a2lem7  10319  hsmexlem4  10342  hsmexlem5  10343  fpwwe2cbv  10544  fpwwe2lem3  10547  fpwwe2lem12  10556  fpwwecbv  10558  canth4  10561  resunimafz0  14398  limsupgval  15429  isercoll  15621  vdwlem1  16943  vdwlem6  16948  vdwlem7  16949  vdwlem8  16950  vdwlem12  16954  vdwlem13  16955  vdwnn  16960  0ram  16982  ramz2  16986  isacs1i  17614  acsficl  18504  gsumvalx  18635  gsumpropd  18637  gsumpropd2lem  18638  gsumress  18641  efgrelexlema  19715  gsumval3a  19869  gsumval3lem1  19871  gsum2dlem2  19937  gsum2d2  19940  dprddisj  19977  dprdf1o  20000  dprdsn  20004  dprd2dlem2  20008  dprd2dlem1  20009  dprd2da  20010  dprd2db  20011  dmdprdsplit2lem  20013  dpjfval  20023  rngqiprngimf1  21293  frlmup3  21775  islindf  21787  islindf2  21789  lindfind  21791  f1lindf  21797  lmimlbs  21811  coe1mul2lem2  22254  subbascn  23237  cncls2  23256  cncls  23257  cnntr  23258  cnpresti  23271  cnprest  23272  cnt1  23333  cnhaus  23337  cncmp  23375  cnconn  23405  1stcfb  23428  xkoccn  23602  ptrescn  23622  xkococnlem  23642  qtopeu  23699  qtoprest  23700  kqdisj  23715  kqcldsat  23716  ordthmeolem  23784  fmfnfmlem4  23940  ustuqtoplem  24222  utopsnneiplem  24230  utopsnneip  24231  ucncn  24267  metustto  24536  metustexhalf  24539  metustfbas  24540  cfilucfil  24542  metuust  24543  cfilucfil2  24544  metuel  24547  metuel2  24548  psmetutop  24550  restmetu  24553  metucn  24554  pi1addval  25033  iscph  25155  cphsscph  25236  uniioombllem3  25570  dyadmbl  25585  mbfima  25615  mbfimaicc  25616  mbfimasn  25617  ismbfd  25624  ismbf2d  25625  ismbf3d  25639  mbfimaopnlem  25640  i1fd  25666  i1f1  25675  itg11  25676  i1faddlem  25678  i1fmullem  25679  i1fadd  25680  itg1addlem3  25683  itg1mulc  25689  itg2gt0  25745  limcnlp  25863  ellimc3  25864  limcflf  25866  limciun  25879  mdegval  26046  mdeg0  26053  mdegvsca  26059  mdegpropd  26067  deg1val  26079  ig1pval  26159  coeeu  26208  coeeq  26210  pserulm  26405  areambl  26940  cutsval  27790  madeval  27842  addbday  28028  negsval  28035  bdayons  28286  zcuts0  28418  bdaypw2n0bndlem  28473  dfpth2  29815  pthdlem2  29854  cyclnumvtx  29886  eupth2lem3  30324  eupth2  30327  issh  31297  isch  31311  shsval  31401  2ndimaxp  32738  fnpreimac  32762  dfcnv2  32767  mptiffisupp  32785  indsupp  32946  indfsid  32948  s2rnOLD  33023  s3rnOLD  33025  swrdrndisj  33036  pwrssmgc  33079  gsummpt2co  33129  gsumpart  33144  gsumhashmul  33148  cycpmco2rn  33206  qusrn  33492  elrspunidl  33511  rhmimaidl  33515  r1pquslmic  33694  psrbasfsupp  33695  esplyfval  33747  esplyfval0  33748  esplyfval2  33749  vieta  33764  dimval  33785  dimvalfi  33786  ply1degltdimlem  33806  extdgval  33837  algextdeglem3  33903  algextdeglem4  33904  algextdeglem5  33905  smatrcl  33980  locfinreflem  34024  zarclsint  34056  rhmpreimacn  34069  zrhunitpreima  34160  mbfmco2  34449  sibfima  34522  sibfof  34524  eulerpartlemgv  34557  eulerpartlemn  34565  eulerpart  34566  orvcval4  34645  orvcelval  34653  orvcelel  34654  ballotlemscr  34703  fnrelpredd  35272  fineqvr1ombregs  35319  f1resfz0f1d  35342  pthhashvtx  35356  erdszelem3  35421  erdsze  35430  cvmliftlem3  35515  cvmliftlem7  35519  cvmlift2lem9a  35531  msrval  35766  mvtinf  35783  mclsval  35791  mclsax  35797  mthmpps  35810  opelco3  36003  funpartlem  36170  tailval  36601  ptrest  37986  poimirlem1  37988  poimirlem2  37989  poimirlem3  37990  poimirlem4  37991  poimirlem5  37992  poimirlem6  37993  poimirlem7  37994  poimirlem9  37996  poimirlem10  37997  poimirlem11  37998  poimirlem12  37999  poimirlem13  38000  poimirlem14  38001  poimirlem15  38002  poimirlem16  38003  poimirlem17  38004  poimirlem19  38006  poimirlem20  38007  poimirlem22  38009  poimirlem23  38010  poimirlem24  38011  poimirlem25  38012  poimirlem26  38013  poimirlem27  38014  poimirlem28  38015  poimirlem29  38016  poimirlem31  38018  poimirlem32  38019  mblfinlem2  38025  volsupnfl  38032  itg2addnclem2  38039  sstotbnd2  38141  ismtyhmeolem  38171  grpokerinj  38260  lkrfval  39579  aks6d1c6lem5  42662  aks6d1c7lem3  42667  dnnumch3lem  43491  aomclem8  43506  pwfi2f1o  43541  cytpval  43647  frege97d  44196  frege109d  44201  frege131d  44208  nzprmdif  44763  relpfrlem  45397  wessf1ornlem  45632  limsuplesup  46142  limsupvaluz  46151  limsuplt2  46196  limsupge  46204  liminfgval  46205  liminfval2  46211  liminflelimsuplem  46218  liminflelimsup  46219  preimaioomnf  47162  fcoreslem2  47527  f1cof1blem  47537  3f1oss1  47538  afv2co2  47720  imarnf1pr  47745  preimafvelsetpreimafv  47863  imaelsetpreimafv  47870  imasetpreimafvbijlemfo  47880  fundcmpsurbijinjpreimafv  47882  fundcmpsurinj  47884  fundcmpsurbijinj  47885  isgrim  48373  grimuhgr  48378  grimcnv  48379  grimco  48380  uhgrimedgi  48381  isuspgrim0lem  48384  isuspgrim0  48385  upgrimwlklem3  48390  upgrimtrls  48397  upgrimpths  48400  gricushgr  48408  cycldlenngric  48419  isubgrgrim  48420  uhgrimisgrgriclem  48421  clnbgrgrimlem  48424  clnbgrgrim  48425  grimedg  48426  cycl3grtri  48438  isubgr3stgrlem4  48460  uspgrlimlem3  48481  predisj  49301  imasubclem3  49596