Theorem imaeq1d 5895

Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)

Hypothesis

Ref	Expression
imaeq1d.1	⊢ (𝜑 → 𝐴 = 𝐵)

Assertion

Ref	Expression
imaeq1d	⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Proof of Theorem imaeq1d

Step	Hyp	Ref	Expression
1		imaeq1d.1	. 2 ⊢ (𝜑 → 𝐴 = 𝐵)
2		imaeq1 5891	. 2 ⊢ (𝐴 = 𝐵 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))
3	1, 2	syl 17	1 ⊢ (𝜑 → (𝐴 “ 𝐶) = (𝐵 “ 𝐶))

Syntax hints:   → wi 4   = wceq 1538   “ cima 5522

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532

This theorem is referenced by:  imaeq12d  5897  nfimad  5905  csbrn  6027  f1imacnv  6606  foimacnv  6607  fimacnvinrn  6817  seqomeq12  8073  ssenen  8675  fipreima  8814  oieq1  8960  oieq2  8961  dfac12lem1  9554  dfac12r  9557  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwecbv  10055  fpwwelem  10056  seqeq1  13367  seqeq2  13368  seqeq3  13369  1arith  16253  vdwmc  16304  vdwnnlem1  16321  ramub2  16340  rami  16341  imasless  16805  gsumvalx  17878  eqglact  18323  psgnunilem1  18613  evpmss  20275  psgnevpmb  20276  frlmup3  20489  psrbag  20602  psrbaglefi  20610  iscn  21840  ptbasfi  22186  ptval2  22206  ptrescn  22244  xkoptsub  22259  qtopval  22300  cmphaushmeo  22405  ptcmpg  22662  restutopopn  22844  prdsxmslem2  23136  metuval  23156  nghmfval  23328  isnghm  23329  ismbf1  24228  ismbf  24232  mbfconst  24237  mbfres2  24249  cncombf  24262  isi1f  24278  itg1val  24287  deg1val  24697  fta1glem2  24767  fta1g  24768  fta1b  24770  dgrval  24825  dgrlem  24826  coeidlem  24834  coe11  24850  fta1lem  24903  fta1  24904  vieta1lem2  24907  vieta1  24908  taylthlem2  24969  areaval  25550  sqff1o  25767  nlfnval  29664  xppreima2  30413  ofpreima  30428  fpwrelmapffslem  30494  evpmval  30837  altgnsg  30841  xrhval  31369  indf1ofs  31395  ismbfm  31620  mbfmcst  31627  issibf  31701  sitgfval  31709  eulerpartlemelr  31725  eulerpartleme  31731  eulerpartlemo  31733  eulerpartlemt0  31737  eulerpartlemt  31739  eulerpartlemr  31742  eulerpartlemgf  31747  eulerpartlemgs2  31748  eulerpartlemn  31749  eulerpart  31750  ballotlemscr  31886  ballotlemrv  31887  ballotlemrinv0  31900  iscvm  32619  cvmliftmolem1  32641  cvmlift2lem9a  32663  cvmlift2lem9  32671  msrfval  32897  ismfs  32909  mthmval  32935  bj-imdirval2  34598  bj-iminvval2  34609  poimirlem4  35061  poimirlem5  35062  poimirlem6  35063  poimirlem7  35064  poimirlem8  35065  poimirlem10  35067  poimirlem11  35068  poimirlem12  35069  poimirlem13  35070  poimirlem14  35071  poimirlem15  35072  poimirlem16  35073  poimirlem17  35074  poimirlem18  35075  poimirlem19  35076  poimirlem20  35077  poimirlem21  35078  poimirlem22  35079  poimirlem26  35083  poimirlem27  35084  poimirlem32  35089  cnambfre  35105  itg2addnclem2  35109  ftc1anclem1  35130  ftc1anclem6  35135  lkrval  36384  pw2f1o2val  39980  aomclem8  40005  pwfi2f1o  40040  trclimalb2  40427  frege131d  40465  colleq12d  40961  dirkercncflem2  42746  issmflem  43361  smfpimioo  43419  smfpimcc  43439  smfsuplem2  43443