Theorem imaeq2d 5931

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

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

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-rab 3149  df-v 3498  df-dif 3941  df-un 3943  df-in 3945  df-ss 3954  df-nul 4294  df-if 4470  df-sn 4570  df-pr 4572  df-op 4576  df-br 5069  df-opab 5131  df-xp 5563  df-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  imaeq12d  5932  nfimad  5940  csbima12  5949  elimasng  5957  elimasni  5958  inisegn0  5963  csbrn  6062  ressn  6138  foima  6597  f1imacnv  6633  dffv3  6668  fvco2  6760  fimacnvinrn2  6843  fsn2  6900  funfvima3  7000  isofrlem  7095  isoselem  7096  fnexALT  7654  curry1  7801  curry2  7804  fparlem3  7811  fparlem4  7812  suppsnop  7846  ressuppssdif  7853  suppco  7872  imacosupp  7876  imacosuppOLD  7877  eceq1  8329  uniqs2  8361  ecinxp  8374  mapsnd  8452  sbthlem2  8630  sbth  8639  phplem4  8701  php3  8705  marypha1lem  8899  cantnfp1lem3  9145  tcrank  9315  fin4en1  9733  fin1a2lem7  9830  hsmexlem4  9853  hsmexlem5  9854  fpwwe2cbv  10054  fpwwe2lem3  10057  fpwwe2lem13  10066  fpwwecbv  10068  canth4  10071  frnnn0fsupp  11957  resunimafz0  13806  limsupgval  14835  isercoll  15026  vdwlem1  16319  vdwlem6  16324  vdwlem7  16325  vdwlem8  16326  vdwlem12  16330  vdwlem13  16331  vdwnn  16336  0ram  16358  ramz2  16362  isacs1i  16930  acsficl  17783  gsumvalx  17888  gsumpropd  17890  gsumpropd2lem  17891  gsumress  17894  efgrelexlema  18877  gsumval3a  19025  gsumval3lem1  19027  gsum2dlem2  19093  gsum2d2  19096  dprddisj  19133  dprdf1o  19156  dprdsn  19160  dprd2dlem2  19164  dprd2dlem1  19165  dprd2da  19166  dprd2db  19167  dmdprdsplit2lem  19169  dpjfval  19179  coe1mul2lem2  20438  frlmup3  20946  islindf  20958  islindf2  20960  lindfind  20962  f1lindf  20968  lmimlbs  20982  subbascn  21864  cncls2  21883  cncls  21884  cnntr  21885  cnpresti  21898  cnprest  21899  cnt1  21960  cnhaus  21964  cncmp  22002  cnconn  22032  1stcfb  22055  xkoccn  22229  ptrescn  22249  xkococnlem  22269  qtopeu  22326  qtoprest  22327  kqdisj  22342  kqcldsat  22343  ordthmeolem  22411  fmfnfmlem4  22567  ustuqtoplem  22850  utopsnneiplem  22858  utopsnneip  22859  ucncn  22896  metustto  23165  metustexhalf  23168  metustfbas  23169  cfilucfil  23171  metuust  23172  cfilucfil2  23173  metuel  23176  metuel2  23177  psmetutop  23179  restmetu  23182  metucn  23183  pi1addval  23654  iscph  23776  cphsscph  23856  uniioombllem3  24188  dyadmbl  24203  mbfima  24233  mbfimaicc  24234  mbfimasn  24235  ismbfd  24242  ismbf2d  24243  ismbf3d  24257  mbfimaopnlem  24258  i1fd  24284  i1f1  24293  itg11  24294  i1faddlem  24296  i1fmullem  24297  i1fadd  24298  itg1addlem3  24301  itg1mulc  24307  itg2gt0  24363  limcnlp  24478  ellimc3  24479  limcflf  24481  limciun  24494  mdegval  24659  mdeg0  24666  mdegvsca  24672  mdegpropd  24680  deg1val  24692  ig1pval  24768  coeeu  24817  coeeq  24819  pserulm  25012  areambl  25538  pthdlem2  27551  eupth2lem3  28017  eupth2  28020  issh  28987  isch  29001  shsval  29091  sspreima  30394  fnpreimac  30418  dfcnv2  30424  s2rn  30622  s3rn  30624  swrdrndisj  30633  gsummpt2co  30688  cycpmco2rn  30769  dimval  31003  dimvalfi  31004  extdgval  31046  smatrcl  31063  locfinreflem  31106  zrhunitpreima  31221  mbfmco2  31525  sibfima  31598  sibfof  31600  eulerpartlemgv  31633  eulerpartlemn  31641  eulerpart  31642  orvcval4  31720  orvcelval  31728  orvcelel  31729  ballotlemscr  31778  f1resfz0f1d  32363  pthhashvtx  32376  erdszelem3  32442  erdsze  32451  cvmliftlem3  32536  cvmliftlem7  32540  cvmlift2lem9a  32552  msrval  32787  mvtinf  32804  mclsval  32812  mclsax  32818  mthmpps  32831  opelco3  33020  scutval  33267  madeval  33291  funpartlem  33405  tailval  33723  csbpredg  34609  ptrest  34893  poimirlem1  34895  poimirlem2  34896  poimirlem3  34897  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem9  34903  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem19  34913  poimirlem20  34914  poimirlem22  34916  poimirlem23  34917  poimirlem24  34918  poimirlem25  34919  poimirlem26  34920  poimirlem27  34921  poimirlem28  34922  poimirlem29  34923  poimirlem31  34925  poimirlem32  34926  mblfinlem2  34932  volsupnfl  34939  itg2addnclem2  34946  sstotbnd2  35054  ismtyhmeolem  35084  grpokerinj  35173  lkrfval  36225  dnnumch3lem  39653  aomclem8  39668  pwfi2f1o  39703  cytpval  39816  frege97d  40104  frege109d  40109  frege131d  40116  nzprmdif  40658  wessf1ornlem  41452  limsuplesup  41987  limsupvaluz  41996  limsuplt2  42041  limsupge  42049  liminfgval  42050  liminfval2  42056  liminflelimsuplem  42063  liminflelimsup  42064  preimaioomnf  43004  afv2co2  43463  imarnf1pr  43488  preimafvelsetpreimafv  43555  imaelsetpreimafv  43562  imasetpreimafvbijlemfo  43572  fundcmpsurbijinjpreimafv  43574  fundcmpsurinj  43576  fundcmpsurbijinj  43577  isomgr  43995  isomushgr  43998  isomgrsym  44008  isomgrtrlem  44010