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 1542   “ cima 5680

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-rab 3434  df-v 3477  df-dif 3952  df-un 3954  df-in 3956  df-ss 3966  df-nul 4324  df-if 4530  df-sn 4630  df-pr 4632  df-op 4636  df-br 5150  df-opab 5212  df-xp 5683  df-cnv 5685  df-dm 5687  df-rn 5688  df-res 5689  df-ima 5690

This theorem is referenced by:  imaeq12d  6061  nfimad  6069  csbima12  6079  elimasngOLD  6090  elimasni  6091  inisegn0  6098  csbrn  6203  ressn  6285  csbpredg  6307  predprc  6340  fncofn  6667  foima  6811  focnvimacdmdm  6818  f1imacnv  6850  dffv3  6888  fvco2  6989  sspreima  7070  fimacnvinrn2  7075  rescnvimafod  7076  fsn2  7134  funfvima3  7238  isofrlem  7337  isoselem  7338  fnexALT  7937  curry1  8090  curry2  8093  fparlem3  8100  fparlem4  8101  suppsnop  8163  ressuppssdif  8170  suppco  8191  imacosupp  8194  naddcllem  8675  eceq1  8741  uniqs2  8773  ecinxp  8786  mapsnd  8880  sbthlem2  9084  sbth  9093  sbthfi  9202  phplem2  9208  php3  9212  phplem4OLD  9220  php3OLD  9224  marypha1lem  9428  cantnfp1lem3  9675  tcrank  9879  fin4en1  10304  fin1a2lem7  10401  hsmexlem4  10424  hsmexlem5  10425  fpwwe2cbv  10625  fpwwe2lem3  10628  fpwwe2lem12  10637  fpwwecbv  10639  canth4  10642  resunimafz0  14404  limsupgval  15420  isercoll  15614  vdwlem1  16914  vdwlem6  16919  vdwlem7  16920  vdwlem8  16921  vdwlem12  16925  vdwlem13  16926  vdwnn  16931  0ram  16953  ramz2  16957  isacs1i  17601  acsficl  18500  gsumvalx  18595  gsumpropd  18597  gsumpropd2lem  18598  gsumress  18601  efgrelexlema  19617  gsumval3a  19771  gsumval3lem1  19773  gsum2dlem2  19839  gsum2d2  19842  dprddisj  19879  dprdf1o  19902  dprdsn  19906  dprd2dlem2  19910  dprd2dlem1  19911  dprd2da  19912  dprd2db  19913  dmdprdsplit2lem  19915  dpjfval  19925  frlmup3  21355  islindf  21367  islindf2  21369  lindfind  21371  f1lindf  21377  lmimlbs  21391  coe1mul2lem2  21790  subbascn  22758  cncls2  22777  cncls  22778  cnntr  22779  cnpresti  22792  cnprest  22793  cnt1  22854  cnhaus  22858  cncmp  22896  cnconn  22926  1stcfb  22949  xkoccn  23123  ptrescn  23143  xkococnlem  23163  qtopeu  23220  qtoprest  23221  kqdisj  23236  kqcldsat  23237  ordthmeolem  23305  fmfnfmlem4  23461  ustuqtoplem  23744  utopsnneiplem  23752  utopsnneip  23753  ucncn  23790  metustto  24062  metustexhalf  24065  metustfbas  24066  cfilucfil  24068  metuust  24069  cfilucfil2  24070  metuel  24073  metuel2  24074  psmetutop  24076  restmetu  24079  metucn  24080  pi1addval  24564  iscph  24687  cphsscph  24768  uniioombllem3  25102  dyadmbl  25117  mbfima  25147  mbfimaicc  25148  mbfimasn  25149  ismbfd  25156  ismbf2d  25157  ismbf3d  25171  mbfimaopnlem  25172  i1fd  25198  i1f1  25207  itg11  25208  i1faddlem  25210  i1fmullem  25211  i1fadd  25212  itg1addlem3  25215  itg1mulc  25222  itg2gt0  25278  limcnlp  25395  ellimc3  25396  limcflf  25398  limciun  25411  mdegval  25581  mdeg0  25588  mdegvsca  25594  mdegpropd  25602  deg1val  25614  ig1pval  25690  coeeu  25739  coeeq  25741  pserulm  25934  areambl  26463  scutval  27302  madeval  27348  negsval  27503  pthdlem2  29056  eupth2lem3  29520  eupth2  29523  issh  30492  isch  30506  shsval  30596  2ndimaxp  31903  fnpreimac  31927  dfcnv2  31932  mptiffisupp  31946  s2rn  32141  s3rn  32143  swrdrndisj  32152  pwrssmgc  32201  gsummpt2co  32231  gsumpart  32238  gsumhashmul  32239  cycpmco2rn  32315  qusrn  32551  elrspunidl  32577  rhmimaidl  32581  dimval  32717  dimvalfi  32718  ply1degltdimlem  32738  extdgval  32764  algextdeglem1  32803  smatrcl  32807  locfinreflem  32851  zarclsint  32883  rhmpreimacn  32896  zrhunitpreima  32989  mbfmco2  33295  sibfima  33368  sibfof  33370  eulerpartlemgv  33403  eulerpartlemn  33411  eulerpart  33412  orvcval4  33490  orvcelval  33498  orvcelel  33499  ballotlemscr  33548  fnrelpredd  34123  f1resfz0f1d  34134  pthhashvtx  34149  erdszelem3  34215  erdsze  34224  cvmliftlem3  34309  cvmliftlem7  34313  cvmlift2lem9a  34325  msrval  34560  mvtinf  34577  mclsval  34585  mclsax  34591  mthmpps  34604  opelco3  34777  funpartlem  34945  tailval  35306  ptrest  36535  poimirlem1  36537  poimirlem2  36538  poimirlem3  36539  poimirlem4  36540  poimirlem5  36541  poimirlem6  36542  poimirlem7  36543  poimirlem9  36545  poimirlem10  36546  poimirlem11  36547  poimirlem12  36548  poimirlem13  36549  poimirlem14  36550  poimirlem15  36551  poimirlem16  36552  poimirlem17  36553  poimirlem19  36555  poimirlem20  36556  poimirlem22  36558  poimirlem23  36559  poimirlem24  36560  poimirlem25  36561  poimirlem26  36562  poimirlem27  36563  poimirlem28  36564  poimirlem29  36565  poimirlem31  36567  poimirlem32  36568  mblfinlem2  36574  volsupnfl  36581  itg2addnclem2  36588  sstotbnd2  36690  ismtyhmeolem  36720  grpokerinj  36809  lkrfval  38005  dnnumch3lem  41836  aomclem8  41851  pwfi2f1o  41886  cytpval  41999  frege97d  42551  frege109d  42556  frege131d  42563  nzprmdif  43126  wessf1ornlem  43930  limsuplesup  44463  limsupvaluz  44472  limsuplt2  44517  limsupge  44525  liminfgval  44526  liminfval2  44532  liminflelimsuplem  44539  liminflelimsup  44540  preimaioomnf  45483  fcoreslem2  45822  f1cof1blem  45832  afv2co2  46013  imarnf1pr  46038  preimafvelsetpreimafv  46104  imaelsetpreimafv  46111  imasetpreimafvbijlemfo  46121  fundcmpsurbijinjpreimafv  46123  fundcmpsurinj  46125  fundcmpsurbijinj  46126  isomgr  46539  isomushgr  46542  isomgrsym  46552  isomgrtrlem  46554  rngqiprngimf1  46833  predisj  47543