Theorem imaeq2d 5764

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

Syntax hints:   → wi 4   = wceq 1507   “ cima 5403

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1758  ax-4 1772  ax-5 1869  ax-6 1928  ax-7 1964  ax-8 2050  ax-9 2057  ax-10 2077  ax-11 2091  ax-12 2104  ax-ext 2745

This theorem depends on definitions:  df-bi 199  df-an 388  df-or 834  df-3an 1070  df-tru 1510  df-ex 1743  df-nf 1747  df-sb 2014  df-clab 2754  df-cleq 2765  df-clel 2840  df-nfc 2912  df-rab 3091  df-v 3411  df-dif 3828  df-un 3830  df-in 3832  df-ss 3839  df-nul 4174  df-if 4345  df-sn 4436  df-pr 4438  df-op 4442  df-br 4924  df-opab 4986  df-xp 5406  df-cnv 5408  df-dm 5410  df-rn 5411  df-res 5412  df-ima 5413

This theorem is referenced by:  imaeq12d  5765  nfimad  5773  csbima12  5781  elimasng  5789  elimasni  5790  inisegn0  5795  csbrn  5893  ressn  5968  foima  6418  f1imacnv  6454  dffv3  6489  fvco2  6580  fimacnvinrn2  6660  fsn2  6715  funfvima3  6817  isofrlem  6910  isoselem  6911  fnexALT  7458  curry1  7600  curry2  7603  fparlem3  7610  fparlem4  7611  suppsnop  7640  ressuppssdif  7647  suppco  7666  imacosupp  7670  imacosuppOLD  7671  eceq1  8119  uniqs2  8151  ecinxp  8164  mapsnd  8240  sbthlem2  8416  sbth  8425  phplem4  8487  php3  8491  marypha1lem  8684  cantnfp1lem3  8929  tcrank  9099  fin4en1  9521  fin1a2lem7  9618  hsmexlem4  9641  hsmexlem5  9642  fpwwe2cbv  9842  fpwwe2lem3  9845  fpwwe2lem13  9854  fpwwecbv  9856  canth4  9859  frnnn0fsupp  11759  resunimafz0  13606  limsupgval  14684  isercoll  14875  vdwlem1  16163  vdwlem6  16168  vdwlem7  16169  vdwlem8  16170  vdwlem12  16174  vdwlem13  16175  vdwnn  16180  0ram  16202  ramz2  16206  isacs1i  16776  acsficl  17629  gsumvalx  17728  gsumpropd  17730  gsumpropd2lem  17731  gsumress  17734  efgrelexlema  18625  gsumval3a  18767  gsumval3lem1  18769  gsum2dlem2  18834  gsum2d2  18837  dprddisj  18871  dprdf1o  18894  dprdsn  18898  dprd2dlem2  18902  dprd2dlem1  18903  dprd2da  18904  dprd2db  18905  dmdprdsplit2lem  18907  dpjfval  18917  coe1mul2lem2  20129  frlmup3  20636  islindf  20648  islindf2  20650  lindfind  20652  f1lindf  20658  lmimlbs  20672  subbascn  21556  cncls2  21575  cncls  21576  cnntr  21577  cnpresti  21590  cnprest  21591  cnt1  21652  cnhaus  21656  cncmp  21694  cnconn  21724  1stcfb  21747  xkoccn  21921  ptrescn  21941  xkococnlem  21961  qtopeu  22018  qtoprest  22019  kqdisj  22034  kqcldsat  22035  ordthmeolem  22103  fmfnfmlem4  22259  ustuqtoplem  22541  utopsnneiplem  22549  utopsnneip  22550  ucncn  22587  metustto  22856  metustexhalf  22859  metustfbas  22860  cfilucfil  22862  metuust  22863  cfilucfil2  22864  metuel  22867  metuel2  22868  psmetutop  22870  restmetu  22873  metucn  22874  pi1addval  23345  iscph  23467  cphsscph  23547  uniioombllem3  23879  dyadmbl  23894  mbfima  23924  mbfimaicc  23925  mbfimasn  23926  ismbfd  23933  ismbf2d  23934  ismbf3d  23948  mbfimaopnlem  23949  i1fd  23975  i1f1  23984  itg11  23985  i1faddlem  23987  i1fmullem  23988  i1fadd  23989  itg1addlem3  23992  itg1mulc  23998  itg2gt0  24054  limcnlp  24169  ellimc3  24170  limcflf  24172  limciun  24185  mdegval  24350  mdeg0  24357  mdegvsca  24363  mdegpropd  24371  deg1val  24383  ig1pval  24459  coeeu  24508  coeeq  24510  pserulm  24703  areambl  25228  pthdlem2  27247  eupth2lem3  27756  eupth2  27759  issh  28754  isch  28768  shsval  28860  sspreima  30144  fnpreimac  30168  dfcnv2  30174  gsummpt2co  30479  dimval  30586  dimvalfi  30587  extdgval  30629  smatrcl  30660  locfinreflem  30705  zrhunitpreima  30820  mbfmco2  31125  sibfima  31198  sibfof  31200  eulerpartlemgv  31233  eulerpartlemn  31241  eulerpart  31242  orvcval4  31321  orvcelval  31329  orvcelel  31330  ballotlemscr  31379  erdszelem3  31985  erdsze  31994  cvmliftlem3  32079  cvmliftlem7  32083  cvmlift2lem9a  32095  msrval  32245  mvtinf  32262  mclsval  32270  mclsax  32276  mthmpps  32289  opelco3  32478  scutval  32726  madeval  32750  funpartlem  32864  tailval  33182  csbpredg  33984  ptrest  34280  poimirlem1  34282  poimirlem2  34283  poimirlem3  34284  poimirlem4  34285  poimirlem5  34286  poimirlem6  34287  poimirlem7  34288  poimirlem9  34290  poimirlem10  34291  poimirlem11  34292  poimirlem12  34293  poimirlem13  34294  poimirlem14  34295  poimirlem15  34296  poimirlem16  34297  poimirlem17  34298  poimirlem19  34300  poimirlem20  34301  poimirlem22  34303  poimirlem23  34304  poimirlem24  34305  poimirlem25  34306  poimirlem26  34307  poimirlem27  34308  poimirlem28  34309  poimirlem29  34310  poimirlem31  34312  poimirlem32  34313  mblfinlem2  34319  volsupnfl  34326  itg2addnclem2  34333  sstotbnd2  34442  ismtyhmeolem  34472  grpokerinj  34561  lkrfval  35616  dnnumch3lem  38987  aomclem8  39002  pwfi2f1o  39037  cytpval  39150  frege97d  39405  frege109d  39410  frege131d  39417  nzprmdif  40011  wessf1ornlem  40815  limsuplesup  41357  limsupvaluz  41366  limsuplt2  41411  limsupge  41419  liminfgval  41420  liminfval2  41426  liminflelimsuplem  41433  liminflelimsup  41434  preimaioomnf  42374  afv2co2  42808  imarnf1pr  42833  isomgr  43296  isomushgr  43299  isomgrsym  43309  isomgrtrlem  43311