Theorem imaeq2d 6031

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

Syntax hints:   → wi 4   = wceq 1540   “ cima 5641

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-rab 3406  df-v 3449  df-dif 3917  df-un 3919  df-in 3921  df-ss 3931  df-nul 4297  df-if 4489  df-sn 4590  df-pr 4592  df-op 4596  df-br 5108  df-opab 5170  df-xp 5644  df-cnv 5646  df-dm 5648  df-rn 5649  df-res 5650  df-ima 5651

This theorem is referenced by:  imaeq12d  6032  nfimad  6040  csbima12  6050  elimasni  6062  inisegn0  6069  csbrn  6176  ressn  6258  csbpredg  6280  predprc  6311  fncofn  6635  foima  6777  focnvimacdmdm  6784  f1imacnv  6816  dffv3  6854  fvco2  6958  sspreima  7040  fimacnvinrn2  7044  rescnvimafod  7045  fsn2  7108  funfvima3  7210  isofrlem  7315  isoselem  7316  fnexALT  7929  mptcnfimad  7965  curry1  8083  curry2  8086  fparlem3  8093  fparlem4  8094  suppsnop  8157  ressuppssdif  8164  suppco  8185  imacosupp  8188  naddcllem  8640  eceq1  8710  uniqs2  8750  ecinxp  8765  mapsnd  8859  sbthlem2  9052  sbth  9061  sbthfi  9163  phplem2  9169  php3  9173  marypha1lem  9384  cantnfp1lem3  9633  tcrank  9837  fin4en1  10262  fin1a2lem7  10359  hsmexlem4  10382  hsmexlem5  10383  fpwwe2cbv  10583  fpwwe2lem3  10586  fpwwe2lem12  10595  fpwwecbv  10597  canth4  10600  resunimafz0  14410  limsupgval  15442  isercoll  15634  vdwlem1  16952  vdwlem6  16957  vdwlem7  16958  vdwlem8  16959  vdwlem12  16963  vdwlem13  16964  vdwnn  16969  0ram  16991  ramz2  16995  isacs1i  17618  acsficl  18506  gsumvalx  18603  gsumpropd  18605  gsumpropd2lem  18606  gsumress  18609  efgrelexlema  19679  gsumval3a  19833  gsumval3lem1  19835  gsum2dlem2  19901  gsum2d2  19904  dprddisj  19941  dprdf1o  19964  dprdsn  19968  dprd2dlem2  19972  dprd2dlem1  19973  dprd2da  19974  dprd2db  19975  dmdprdsplit2lem  19977  dpjfval  19987  rngqiprngimf1  21210  frlmup3  21709  islindf  21721  islindf2  21723  lindfind  21725  f1lindf  21731  lmimlbs  21745  coe1mul2lem2  22154  subbascn  23141  cncls2  23160  cncls  23161  cnntr  23162  cnpresti  23175  cnprest  23176  cnt1  23237  cnhaus  23241  cncmp  23279  cnconn  23309  1stcfb  23332  xkoccn  23506  ptrescn  23526  xkococnlem  23546  qtopeu  23603  qtoprest  23604  kqdisj  23619  kqcldsat  23620  ordthmeolem  23688  fmfnfmlem4  23844  ustuqtoplem  24127  utopsnneiplem  24135  utopsnneip  24136  ucncn  24172  metustto  24441  metustexhalf  24444  metustfbas  24445  cfilucfil  24447  metuust  24448  cfilucfil2  24449  metuel  24452  metuel2  24453  psmetutop  24455  restmetu  24458  metucn  24459  pi1addval  24948  iscph  25070  cphsscph  25151  uniioombllem3  25486  dyadmbl  25501  mbfima  25531  mbfimaicc  25532  mbfimasn  25533  ismbfd  25540  ismbf2d  25541  ismbf3d  25555  mbfimaopnlem  25556  i1fd  25582  i1f1  25591  itg11  25592  i1faddlem  25594  i1fmullem  25595  i1fadd  25596  itg1addlem3  25599  itg1mulc  25605  itg2gt0  25661  limcnlp  25779  ellimc3  25780  limcflf  25782  limciun  25795  mdegval  25968  mdeg0  25975  mdegvsca  25981  mdegpropd  25989  deg1val  26001  ig1pval  26081  coeeu  26130  coeeq  26132  pserulm  26331  areambl  26868  scutval  27712  madeval  27760  addsbday  27924  negsval  27931  bdayon  28173  dfpth2  29659  pthdlem2  29698  cyclnumvtx  29730  eupth2lem3  30165  eupth2  30168  issh  31137  isch  31151  shsval  31241  2ndimaxp  32570  fnpreimac  32595  dfcnv2  32600  mptiffisupp  32616  indsupp  32790  s2rnOLD  32865  s3rnOLD  32867  swrdrndisj  32879  pwrssmgc  32926  gsummpt2co  32988  gsumpart  32997  gsumhashmul  33001  cycpmco2rn  33082  qusrn  33380  elrspunidl  33399  rhmimaidl  33403  r1pquslmic  33576  dimval  33596  dimvalfi  33597  ply1degltdimlem  33618  extdgval  33649  algextdeglem3  33709  algextdeglem4  33710  algextdeglem5  33711  smatrcl  33786  locfinreflem  33830  zarclsint  33862  rhmpreimacn  33875  zrhunitpreima  33966  mbfmco2  34256  sibfima  34329  sibfof  34331  eulerpartlemgv  34364  eulerpartlemn  34372  eulerpart  34373  orvcval4  34452  orvcelval  34460  orvcelel  34461  ballotlemscr  34510  fnrelpredd  35079  f1resfz0f1d  35101  pthhashvtx  35115  erdszelem3  35180  erdsze  35189  cvmliftlem3  35274  cvmliftlem7  35278  cvmlift2lem9a  35290  msrval  35525  mvtinf  35542  mclsval  35550  mclsax  35556  mthmpps  35569  opelco3  35762  funpartlem  35930  tailval  36361  ptrest  37613  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem5  37619  poimirlem6  37620  poimirlem7  37621  poimirlem9  37623  poimirlem10  37624  poimirlem11  37625  poimirlem12  37626  poimirlem13  37627  poimirlem14  37628  poimirlem15  37629  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem22  37636  poimirlem23  37637  poimirlem24  37638  poimirlem25  37639  poimirlem26  37640  poimirlem27  37641  poimirlem28  37642  poimirlem29  37643  poimirlem31  37645  poimirlem32  37646  mblfinlem2  37652  volsupnfl  37659  itg2addnclem2  37666  sstotbnd2  37768  ismtyhmeolem  37798  grpokerinj  37887  lkrfval  39080  aks6d1c6lem5  42165  aks6d1c7lem3  42170  dnnumch3lem  43035  aomclem8  43050  pwfi2f1o  43085  cytpval  43191  frege97d  43741  frege109d  43746  frege131d  43753  nzprmdif  44308  relpfrlem  44943  wessf1ornlem  45179  limsuplesup  45697  limsupvaluz  45706  limsuplt2  45751  limsupge  45759  liminfgval  45760  liminfval2  45766  liminflelimsuplem  45773  liminflelimsup  45774  preimaioomnf  46717  fcoreslem2  47065  f1cof1blem  47075  3f1oss1  47076  afv2co2  47258  imarnf1pr  47283  preimafvelsetpreimafv  47389  imaelsetpreimafv  47396  imasetpreimafvbijlemfo  47406  fundcmpsurbijinjpreimafv  47408  fundcmpsurinj  47410  fundcmpsurbijinj  47411  isgrim  47882  grimuhgr  47887  grimcnv  47888  grimco  47889  uhgrimedgi  47890  isuspgrim0lem  47893  isuspgrim0  47894  upgrimwlklem3  47899  upgrimtrls  47906  upgrimpths  47909  gricushgr  47917  cycldlenngric  47928  isubgrgrim  47929  uhgrimisgrgriclem  47930  clnbgrgrimlem  47933  clnbgrgrim  47934  grimedg  47935  cycl3grtri  47946  isubgr3stgrlem4  47968  uspgrlimlem3  47989  predisj  48799  imasubclem3  49095