Theorem imaeq2d 5929

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

Syntax hints:   → wi 4   = wceq 1537   “ cima 5558

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3496  df-dif 3939  df-un 3941  df-in 3943  df-ss 3952  df-nul 4292  df-if 4468  df-sn 4568  df-pr 4570  df-op 4574  df-br 5067  df-opab 5129  df-xp 5561  df-cnv 5563  df-dm 5565  df-rn 5566  df-res 5567  df-ima 5568

This theorem is referenced by:  imaeq12d  5930  nfimad  5938  csbima12  5947  elimasng  5955  elimasni  5956  inisegn0  5961  csbrn  6060  ressn  6136  foima  6595  f1imacnv  6631  dffv3  6666  fvco2  6758  fimacnvinrn2  6841  fsn2  6898  funfvima3  6998  isofrlem  7093  isoselem  7094  fnexALT  7652  curry1  7799  curry2  7802  fparlem3  7809  fparlem4  7810  suppsnop  7844  ressuppssdif  7851  suppco  7870  imacosupp  7874  imacosuppOLD  7875  eceq1  8327  uniqs2  8359  ecinxp  8372  mapsnd  8450  sbthlem2  8628  sbth  8637  phplem4  8699  php3  8703  marypha1lem  8897  cantnfp1lem3  9143  tcrank  9313  fin4en1  9731  fin1a2lem7  9828  hsmexlem4  9851  hsmexlem5  9852  fpwwe2cbv  10052  fpwwe2lem3  10055  fpwwe2lem13  10064  fpwwecbv  10066  canth4  10069  frnnn0fsupp  11955  resunimafz0  13804  limsupgval  14833  isercoll  15024  vdwlem1  16317  vdwlem6  16322  vdwlem7  16323  vdwlem8  16324  vdwlem12  16328  vdwlem13  16329  vdwnn  16334  0ram  16356  ramz2  16360  isacs1i  16928  acsficl  17781  gsumvalx  17886  gsumpropd  17888  gsumpropd2lem  17889  gsumress  17892  efgrelexlema  18875  gsumval3a  19023  gsumval3lem1  19025  gsum2dlem2  19091  gsum2d2  19094  dprddisj  19131  dprdf1o  19154  dprdsn  19158  dprd2dlem2  19162  dprd2dlem1  19163  dprd2da  19164  dprd2db  19165  dmdprdsplit2lem  19167  dpjfval  19177  coe1mul2lem2  20436  frlmup3  20944  islindf  20956  islindf2  20958  lindfind  20960  f1lindf  20966  lmimlbs  20980  subbascn  21862  cncls2  21881  cncls  21882  cnntr  21883  cnpresti  21896  cnprest  21897  cnt1  21958  cnhaus  21962  cncmp  22000  cnconn  22030  1stcfb  22053  xkoccn  22227  ptrescn  22247  xkococnlem  22267  qtopeu  22324  qtoprest  22325  kqdisj  22340  kqcldsat  22341  ordthmeolem  22409  fmfnfmlem4  22565  ustuqtoplem  22848  utopsnneiplem  22856  utopsnneip  22857  ucncn  22894  metustto  23163  metustexhalf  23166  metustfbas  23167  cfilucfil  23169  metuust  23170  cfilucfil2  23171  metuel  23174  metuel2  23175  psmetutop  23177  restmetu  23180  metucn  23181  pi1addval  23652  iscph  23774  cphsscph  23854  uniioombllem3  24186  dyadmbl  24201  mbfima  24231  mbfimaicc  24232  mbfimasn  24233  ismbfd  24240  ismbf2d  24241  ismbf3d  24255  mbfimaopnlem  24256  i1fd  24282  i1f1  24291  itg11  24292  i1faddlem  24294  i1fmullem  24295  i1fadd  24296  itg1addlem3  24299  itg1mulc  24305  itg2gt0  24361  limcnlp  24476  ellimc3  24477  limcflf  24479  limciun  24492  mdegval  24657  mdeg0  24664  mdegvsca  24670  mdegpropd  24678  deg1val  24690  ig1pval  24766  coeeu  24815  coeeq  24817  pserulm  25010  areambl  25536  pthdlem2  27549  eupth2lem3  28015  eupth2  28018  issh  28985  isch  28999  shsval  29089  sspreima  30392  fnpreimac  30416  dfcnv2  30422  s2rn  30620  s3rn  30622  swrdrndisj  30631  gsummpt2co  30686  cycpmco2rn  30767  dimval  31001  dimvalfi  31002  extdgval  31044  smatrcl  31061  locfinreflem  31104  zrhunitpreima  31219  mbfmco2  31523  sibfima  31596  sibfof  31598  eulerpartlemgv  31631  eulerpartlemn  31639  eulerpart  31640  orvcval4  31718  orvcelval  31726  orvcelel  31727  ballotlemscr  31776  f1resfz0f1d  32361  pthhashvtx  32374  erdszelem3  32440  erdsze  32449  cvmliftlem3  32534  cvmliftlem7  32538  cvmlift2lem9a  32550  msrval  32785  mvtinf  32802  mclsval  32810  mclsax  32816  mthmpps  32829  opelco3  33018  scutval  33265  madeval  33289  funpartlem  33403  tailval  33721  csbpredg  34610  ptrest  34906  poimirlem1  34908  poimirlem2  34909  poimirlem3  34910  poimirlem4  34911  poimirlem5  34912  poimirlem6  34913  poimirlem7  34914  poimirlem9  34916  poimirlem10  34917  poimirlem11  34918  poimirlem12  34919  poimirlem13  34920  poimirlem14  34921  poimirlem15  34922  poimirlem16  34923  poimirlem17  34924  poimirlem19  34926  poimirlem20  34927  poimirlem22  34929  poimirlem23  34930  poimirlem24  34931  poimirlem25  34932  poimirlem26  34933  poimirlem27  34934  poimirlem28  34935  poimirlem29  34936  poimirlem31  34938  poimirlem32  34939  mblfinlem2  34945  volsupnfl  34952  itg2addnclem2  34959  sstotbnd2  35067  ismtyhmeolem  35097  grpokerinj  35186  lkrfval  36238  dnnumch3lem  39666  aomclem8  39681  pwfi2f1o  39716  cytpval  39829  frege97d  40117  frege109d  40122  frege131d  40129  nzprmdif  40671  wessf1ornlem  41465  limsuplesup  42000  limsupvaluz  42009  limsuplt2  42054  limsupge  42062  liminfgval  42063  liminfval2  42069  liminflelimsuplem  42076  liminflelimsup  42077  preimaioomnf  43017  afv2co2  43476  imarnf1pr  43501  preimafvelsetpreimafv  43568  imaelsetpreimafv  43575  imasetpreimafvbijlemfo  43585  fundcmpsurbijinjpreimafv  43587  fundcmpsurinj  43589  fundcmpsurbijinj  43590  isomgr  44008  isomushgr  44011  isomgrsym  44021  isomgrtrlem  44023