Theorem imaeq2d 6019

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

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

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 3391  df-v 3432  df-dif 3893  df-un 3895  df-in 3897  df-ss 3907  df-nul 4275  df-if 4468  df-sn 4569  df-pr 4571  df-op 4575  df-br 5087  df-opab 5149  df-xp 5630  df-cnv 5632  df-dm 5634  df-rn 5635  df-res 5636  df-ima 5637

This theorem is referenced by:  imaeq12d  6020  nfimad  6028  csbima12  6038  elimasni  6050  inisegn0  6057  csbrn  6161  ressn  6243  csbpredg  6265  predprc  6296  fncofn  6609  foima  6751  focnvimacdmdm  6758  f1imacnv  6790  dffv3  6830  fvco2  6931  sspreima  7014  fimacnvinrn2  7018  rescnvimafod  7019  fsn2  7083  funfvima3  7184  isofrlem  7288  isoselem  7289  fnexALT  7897  mptcnfimad  7932  curry1  8047  curry2  8050  fparlem3  8057  fparlem4  8058  suppsnop  8121  ressuppssdif  8128  suppco  8149  imacosupp  8152  naddcllem  8605  eceq1  8676  uniqs2  8716  ecinxp  8732  mapsnd  8827  sbthlem2  9019  sbth  9028  sbthfi  9126  phplem2  9132  php3  9136  marypha1lem  9339  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  21290  frlmup3  21790  islindf  21802  islindf2  21804  lindfind  21806  f1lindf  21812  lmimlbs  21826  coe1mul2lem2  22243  subbascn  23229  cncls2  23248  cncls  23249  cnntr  23250  cnpresti  23263  cnprest  23264  cnt1  23325  cnhaus  23329  cncmp  23367  cnconn  23397  1stcfb  23420  xkoccn  23594  ptrescn  23614  xkococnlem  23634  qtopeu  23691  qtoprest  23692  kqdisj  23707  kqcldsat  23708  ordthmeolem  23776  fmfnfmlem4  23932  ustuqtoplem  24214  utopsnneiplem  24222  utopsnneip  24223  ucncn  24259  metustto  24528  metustexhalf  24531  metustfbas  24532  cfilucfil  24534  metuust  24535  cfilucfil2  24536  metuel  24539  metuel2  24540  psmetutop  24542  restmetu  24545  metucn  24546  pi1addval  25025  iscph  25147  cphsscph  25228  uniioombllem3  25562  dyadmbl  25577  mbfima  25607  mbfimaicc  25608  mbfimasn  25609  ismbfd  25616  ismbf2d  25617  ismbf3d  25631  mbfimaopnlem  25632  i1fd  25658  i1f1  25667  itg11  25668  i1faddlem  25670  i1fmullem  25671  i1fadd  25672  itg1addlem3  25675  itg1mulc  25681  itg2gt0  25737  limcnlp  25855  ellimc3  25856  limcflf  25858  limciun  25871  mdegval  26038  mdeg0  26045  mdegvsca  26051  mdegpropd  26059  deg1val  26071  ig1pval  26151  coeeu  26200  coeeq  26202  pserulm  26400  areambl  26935  cutsval  27786  madeval  27838  addbday  28024  negsval  28031  bdayons  28282  zcuts0  28414  bdaypw2n0bndlem  28469  dfpth2  29812  pthdlem2  29851  cyclnumvtx  29883  eupth2lem3  30321  eupth2  30324  issh  31294  isch  31308  shsval  31398  2ndimaxp  32734  fnpreimac  32758  dfcnv2  32763  mptiffisupp  32781  indsupp  32942  indfsid  32944  s2rnOLD  33019  s3rnOLD  33021  swrdrndisj  33032  pwrssmgc  33075  gsummpt2co  33124  gsumpart  33139  gsumhashmul  33143  cycpmco2rn  33201  qusrn  33484  elrspunidl  33503  rhmimaidl  33507  r1pquslmic  33686  psrbasfsupp  33687  esplyfval  33722  esplyfval0  33723  esplyfval2  33724  vieta  33739  dimval  33760  dimvalfi  33761  ply1degltdimlem  33782  extdgval  33813  algextdeglem3  33879  algextdeglem4  33880  algextdeglem5  33881  smatrcl  33956  locfinreflem  34000  zarclsint  34032  rhmpreimacn  34045  zrhunitpreima  34136  mbfmco2  34425  sibfima  34498  sibfof  34500  eulerpartlemgv  34533  eulerpartlemn  34541  eulerpart  34542  orvcval4  34621  orvcelval  34629  orvcelel  34630  ballotlemscr  34679  fnrelpredd  35250  fineqvr1ombregs  35298  f1resfz0f1d  35312  pthhashvtx  35326  erdszelem3  35391  erdsze  35400  cvmliftlem3  35485  cvmliftlem7  35489  cvmlift2lem9a  35501  msrval  35736  mvtinf  35753  mclsval  35761  mclsax  35767  mthmpps  35780  opelco3  35973  funpartlem  36140  tailval  36571  ptrest  37954  poimirlem1  37956  poimirlem2  37957  poimirlem3  37958  poimirlem4  37959  poimirlem5  37960  poimirlem6  37961  poimirlem7  37962  poimirlem9  37964  poimirlem10  37965  poimirlem11  37966  poimirlem12  37967  poimirlem13  37968  poimirlem14  37969  poimirlem15  37970  poimirlem16  37971  poimirlem17  37972  poimirlem19  37974  poimirlem20  37975  poimirlem22  37977  poimirlem23  37978  poimirlem24  37979  poimirlem25  37980  poimirlem26  37981  poimirlem27  37982  poimirlem28  37983  poimirlem29  37984  poimirlem31  37986  poimirlem32  37987  mblfinlem2  37993  volsupnfl  38000  itg2addnclem2  38007  sstotbnd2  38109  ismtyhmeolem  38139  grpokerinj  38228  lkrfval  39547  aks6d1c6lem5  42630  aks6d1c7lem3  42635  dnnumch3lem  43492  aomclem8  43507  pwfi2f1o  43542  cytpval  43648  frege97d  44197  frege109d  44202  frege131d  44209  nzprmdif  44764  relpfrlem  45398  wessf1ornlem  45633  limsuplesup  46145  limsupvaluz  46154  limsuplt2  46199  limsupge  46207  liminfgval  46208  liminfval2  46214  liminflelimsuplem  46221  liminflelimsup  46222  preimaioomnf  47165  fcoreslem2  47524  f1cof1blem  47534  3f1oss1  47535  afv2co2  47717  imarnf1pr  47742  preimafvelsetpreimafv  47860  imaelsetpreimafv  47867  imasetpreimafvbijlemfo  47877  fundcmpsurbijinjpreimafv  47879  fundcmpsurinj  47881  fundcmpsurbijinj  47882  isgrim  48370  grimuhgr  48375  grimcnv  48376  grimco  48377  uhgrimedgi  48378  isuspgrim0lem  48381  isuspgrim0  48382  upgrimwlklem3  48387  upgrimtrls  48394  upgrimpths  48397  gricushgr  48405  cycldlenngric  48416  isubgrgrim  48417  uhgrimisgrgriclem  48418  clnbgrgrimlem  48421  clnbgrgrim  48422  grimedg  48423  cycl3grtri  48435  isubgr3stgrlem4  48457  uspgrlimlem3  48478  predisj  49298  imasubclem3  49593