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  27301  madeval  27347  negsval  27500  pthdlem2  29025  eupth2lem3  29489  eupth2  29492  issh  30461  isch  30475  shsval  30565  2ndimaxp  31872  fnpreimac  31896  dfcnv2  31901  mptiffisupp  31915  s2rn  32110  s3rn  32112  swrdrndisj  32121  pwrssmgc  32170  gsummpt2co  32200  gsumpart  32207  gsumhashmul  32208  cycpmco2rn  32284  qusrn  32520  elrspunidl  32546  rhmimaidl  32550  dimval  32686  dimvalfi  32687  ply1degltdimlem  32707  extdgval  32733  algextdeglem1  32772  smatrcl  32776  locfinreflem  32820  zarclsint  32852  rhmpreimacn  32865  zrhunitpreima  32958  mbfmco2  33264  sibfima  33337  sibfof  33339  eulerpartlemgv  33372  eulerpartlemn  33380  eulerpart  33381  orvcval4  33459  orvcelval  33467  orvcelel  33468  ballotlemscr  33517  fnrelpredd  34092  f1resfz0f1d  34103  pthhashvtx  34118  erdszelem3  34184  erdsze  34193  cvmliftlem3  34278  cvmliftlem7  34282  cvmlift2lem9a  34294  msrval  34529  mvtinf  34546  mclsval  34554  mclsax  34560  mthmpps  34573  opelco3  34746  funpartlem  34914  tailval  35258  ptrest  36487  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem5  36493  poimirlem6  36494  poimirlem7  36495  poimirlem9  36497  poimirlem10  36498  poimirlem11  36499  poimirlem12  36500  poimirlem13  36501  poimirlem14  36502  poimirlem15  36503  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem22  36510  poimirlem23  36511  poimirlem24  36512  poimirlem25  36513  poimirlem26  36514  poimirlem27  36515  poimirlem28  36516  poimirlem29  36517  poimirlem31  36519  poimirlem32  36520  mblfinlem2  36526  volsupnfl  36533  itg2addnclem2  36540  sstotbnd2  36642  ismtyhmeolem  36672  grpokerinj  36761  lkrfval  37957  dnnumch3lem  41788  aomclem8  41803  pwfi2f1o  41838  cytpval  41951  frege97d  42503  frege109d  42508  frege131d  42515  nzprmdif  43078  wessf1ornlem  43882  limsuplesup  44415  limsupvaluz  44424  limsuplt2  44469  limsupge  44477  liminfgval  44478  liminfval2  44484  liminflelimsuplem  44491  liminflelimsup  44492  preimaioomnf  45435  fcoreslem2  45774  f1cof1blem  45784  afv2co2  45965  imarnf1pr  45990  preimafvelsetpreimafv  46056  imaelsetpreimafv  46063  imasetpreimafvbijlemfo  46073  fundcmpsurbijinjpreimafv  46075  fundcmpsurinj  46077  fundcmpsurbijinj  46078  isomgr  46491  isomushgr  46494  isomgrsym  46504  isomgrtrlem  46506  rngqiprngimf1  46785  predisj  47495