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 17	1 ⊢ (𝜑 → (𝐶 “ 𝐴) = (𝐶 “ 𝐵))

Syntax hints:   → wi 4   = wceq 1539   “ cima 5670

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1542  df-fal 1552  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-rab 3421  df-v 3466  df-dif 3936  df-un 3938  df-in 3940  df-ss 3950  df-nul 4316  df-if 4508  df-sn 4609  df-pr 4611  df-op 4615  df-br 5126  df-opab 5188  df-xp 5673  df-cnv 5675  df-dm 5677  df-rn 5678  df-res 5679  df-ima 5680

This theorem is referenced by:  imaeq12d  6061  nfimad  6069  csbima12  6079  elimasni  6091  inisegn0  6098  csbrn  6205  ressn  6287  csbpredg  6309  predprc  6340  fncofn  6666  foima  6806  focnvimacdmdm  6813  f1imacnv  6845  dffv3  6883  fvco2  6987  sspreima  7069  fimacnvinrn2  7073  rescnvimafod  7074  fsn2  7137  funfvima3  7239  isofrlem  7343  isoselem  7344  fnexALT  7958  mptcnfimad  7994  curry1  8112  curry2  8115  fparlem3  8122  fparlem4  8123  suppsnop  8186  ressuppssdif  8193  suppco  8214  imacosupp  8217  naddcllem  8697  eceq1  8767  uniqs2  8802  ecinxp  8815  mapsnd  8909  sbthlem2  9107  sbth  9116  sbthfi  9222  phplem2  9228  php3  9232  phplem4OLD  9240  php3OLD  9244  marypha1lem  9456  cantnfp1lem3  9703  tcrank  9907  fin4en1  10332  fin1a2lem7  10429  hsmexlem4  10452  hsmexlem5  10453  fpwwe2cbv  10653  fpwwe2lem3  10656  fpwwe2lem12  10665  fpwwecbv  10667  canth4  10670  resunimafz0  14467  limsupgval  15495  isercoll  15687  vdwlem1  17002  vdwlem6  17007  vdwlem7  17008  vdwlem8  17009  vdwlem12  17013  vdwlem13  17014  vdwnn  17019  0ram  17041  ramz2  17045  isacs1i  17676  acsficl  18566  gsumvalx  18663  gsumpropd  18665  gsumpropd2lem  18666  gsumress  18669  efgrelexlema  19740  gsumval3a  19894  gsumval3lem1  19896  gsum2dlem2  19962  gsum2d2  19965  dprddisj  20002  dprdf1o  20025  dprdsn  20029  dprd2dlem2  20033  dprd2dlem1  20034  dprd2da  20035  dprd2db  20036  dmdprdsplit2lem  20038  dpjfval  20048  rngqiprngimf1  21277  frlmup3  21787  islindf  21799  islindf2  21801  lindfind  21803  f1lindf  21809  lmimlbs  21823  coe1mul2lem2  22238  subbascn  23227  cncls2  23246  cncls  23247  cnntr  23248  cnpresti  23261  cnprest  23262  cnt1  23323  cnhaus  23327  cncmp  23365  cnconn  23395  1stcfb  23418  xkoccn  23592  ptrescn  23612  xkococnlem  23632  qtopeu  23689  qtoprest  23690  kqdisj  23705  kqcldsat  23706  ordthmeolem  23774  fmfnfmlem4  23930  ustuqtoplem  24213  utopsnneiplem  24221  utopsnneip  24222  ucncn  24258  metustto  24529  metustexhalf  24532  metustfbas  24533  cfilucfil  24535  metuust  24536  cfilucfil2  24537  metuel  24540  metuel2  24541  psmetutop  24543  restmetu  24546  metucn  24547  pi1addval  25036  iscph  25159  cphsscph  25240  uniioombllem3  25575  dyadmbl  25590  mbfima  25620  mbfimaicc  25621  mbfimasn  25622  ismbfd  25629  ismbf2d  25630  ismbf3d  25644  mbfimaopnlem  25645  i1fd  25671  i1f1  25680  itg11  25681  i1faddlem  25683  i1fmullem  25684  i1fadd  25685  itg1addlem3  25688  itg1mulc  25694  itg2gt0  25750  limcnlp  25868  ellimc3  25869  limcflf  25871  limciun  25884  mdegval  26057  mdeg0  26064  mdegvsca  26070  mdegpropd  26078  deg1val  26090  ig1pval  26170  coeeu  26219  coeeq  26221  pserulm  26420  areambl  26956  scutval  27800  madeval  27846  addsbday  28005  negsval  28012  dfpth2  29696  pthdlem2  29735  cyclnumvtx  29767  eupth2lem3  30202  eupth2  30205  issh  31174  isch  31188  shsval  31278  2ndimaxp  32603  fnpreimac  32628  dfcnv2  32633  mptiffisupp  32649  indsupp  32799  s2rnOLD  32875  s3rnOLD  32877  swrdrndisj  32889  pwrssmgc  32936  gsummpt2co  32997  gsumpart  33006  gsumhashmul  33010  cycpmco2rn  33091  qusrn  33378  elrspunidl  33397  rhmimaidl  33401  r1pquslmic  33572  dimval  33592  dimvalfi  33593  ply1degltdimlem  33614  extdgval  33646  algextdeglem3  33701  algextdeglem4  33702  algextdeglem5  33703  smatrcl  33736  locfinreflem  33780  zarclsint  33812  rhmpreimacn  33825  zrhunitpreima  33918  mbfmco2  34208  sibfima  34281  sibfof  34283  eulerpartlemgv  34316  eulerpartlemn  34324  eulerpart  34325  orvcval4  34404  orvcelval  34412  orvcelel  34413  ballotlemscr  34462  fnrelpredd  35044  f1resfz0f1d  35060  pthhashvtx  35074  erdszelem3  35139  erdsze  35148  cvmliftlem3  35233  cvmliftlem7  35237  cvmlift2lem9a  35249  msrval  35484  mvtinf  35501  mclsval  35509  mclsax  35515  mthmpps  35528  opelco3  35716  funpartlem  35884  tailval  36315  ptrest  37567  poimirlem1  37569  poimirlem2  37570  poimirlem3  37571  poimirlem4  37572  poimirlem5  37573  poimirlem6  37574  poimirlem7  37575  poimirlem9  37577  poimirlem10  37578  poimirlem11  37579  poimirlem12  37580  poimirlem13  37581  poimirlem14  37582  poimirlem15  37583  poimirlem16  37584  poimirlem17  37585  poimirlem19  37587  poimirlem20  37588  poimirlem22  37590  poimirlem23  37591  poimirlem24  37592  poimirlem25  37593  poimirlem26  37594  poimirlem27  37595  poimirlem28  37596  poimirlem29  37597  poimirlem31  37599  poimirlem32  37600  mblfinlem2  37606  volsupnfl  37613  itg2addnclem2  37620  sstotbnd2  37722  ismtyhmeolem  37752  grpokerinj  37841  lkrfval  39029  aks6d1c6lem5  42119  aks6d1c7lem3  42124  dnnumch3lem  43003  aomclem8  43018  pwfi2f1o  43053  cytpval  43159  frege97d  43710  frege109d  43715  frege131d  43722  nzprmdif  44283  relpfrlem  44919  wessf1ornlem  45135  limsuplesup  45659  limsupvaluz  45668  limsuplt2  45713  limsupge  45721  liminfgval  45722  liminfval2  45728  liminflelimsuplem  45735  liminflelimsup  45736  preimaioomnf  46679  fcoreslem2  47022  f1cof1blem  47032  3f1oss1  47033  afv2co2  47215  imarnf1pr  47240  preimafvelsetpreimafv  47321  imaelsetpreimafv  47328  imasetpreimafvbijlemfo  47338  fundcmpsurbijinjpreimafv  47340  fundcmpsurinj  47342  fundcmpsurbijinj  47343  isgrim  47814  isuspgrim0lem  47817  isuspgrim0  47818  grimuhgr  47824  grimcnv  47825  grimco  47826  gricushgr  47832  isubgrgrim  47843  uhgrimisgrgriclem  47844  clnbgrgrimlem  47847  clnbgrgrim  47848  grimedg  47849  cycl3grtri  47860  isubgr3stgrlem4  47882  uspgrlimlem3  47903  predisj  48676