Theorem imaeq1d 5931

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

Syntax hints:   → wi 4   = wceq 1536   “ cima 5561

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1969  ax-7 2014  ax-8 2115  ax-9 2123  ax-10 2144  ax-11 2160  ax-12 2176  ax-ext 2796

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-3an 1085  df-tru 1539  df-ex 1780  df-nf 1784  df-sb 2069  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2966  df-rab 3150  df-v 3499  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-nul 4295  df-if 4471  df-sn 4571  df-pr 4573  df-op 4577  df-br 5070  df-opab 5132  df-cnv 5566  df-dm 5568  df-rn 5569  df-res 5570  df-ima 5571

This theorem is referenced by:  imaeq12d  5933  nfimad  5941  csbrn  6063  f1imacnv  6634  foimacnv  6635  fimacnvinrn  6843  seqomeq12  8093  ssenen  8694  fipreima  8833  oieq1  8979  oieq2  8980  dfac12lem1  9572  dfac12r  9575  fpwwe2cbv  10055  fpwwe2lem2  10057  fpwwecbv  10069  fpwwelem  10070  seqeq1  13375  seqeq2  13376  seqeq3  13377  1arith  16266  vdwmc  16317  vdwnnlem1  16334  ramub2  16353  rami  16354  imasless  16816  gsumvalx  17889  eqglact  18334  psgnunilem1  18624  psrbag  20147  psrbaglefi  20155  evpmss  20733  psgnevpmb  20734  frlmup3  20947  iscn  21846  ptbasfi  22192  ptval2  22212  ptrescn  22250  xkoptsub  22265  qtopval  22306  cmphaushmeo  22411  ptcmpg  22668  restutopopn  22850  prdsxmslem2  23142  metuval  23162  nghmfval  23334  isnghm  23335  ismbf1  24228  ismbf  24232  mbfconst  24237  mbfres2  24249  cncombf  24262  isi1f  24278  itg1val  24287  deg1val  24693  fta1glem2  24763  fta1g  24764  fta1b  24766  dgrval  24821  dgrlem  24822  coeidlem  24830  coe11  24846  fta1lem  24899  fta1  24900  vieta1lem2  24903  vieta1  24904  taylthlem2  24965  areaval  25545  sqff1o  25762  nlfnval  29661  xppreima2  30398  ofpreima  30413  fpwrelmapffslem  30471  evpmval  30791  altgnsg  30795  xrhval  31263  indf1ofs  31289  ismbfm  31514  mbfmcst  31521  issibf  31595  sitgfval  31603  eulerpartlemelr  31619  eulerpartleme  31625  eulerpartlemo  31627  eulerpartlemt0  31631  eulerpartlemt  31633  eulerpartlemr  31636  eulerpartlemgf  31641  eulerpartlemgs2  31642  eulerpartlemn  31643  eulerpart  31644  ballotlemscr  31780  ballotlemrv  31781  ballotlemrinv0  31794  iscvm  32510  cvmliftmolem1  32532  cvmlift2lem9a  32554  cvmlift2lem9  32562  msrfval  32788  ismfs  32800  mthmval  32826  bj-imdirval2  34477  poimirlem4  34900  poimirlem5  34901  poimirlem6  34902  poimirlem7  34903  poimirlem8  34904  poimirlem10  34906  poimirlem11  34907  poimirlem12  34908  poimirlem13  34909  poimirlem14  34910  poimirlem15  34911  poimirlem16  34912  poimirlem17  34913  poimirlem18  34914  poimirlem19  34915  poimirlem20  34916  poimirlem21  34917  poimirlem22  34918  poimirlem26  34922  poimirlem27  34923  poimirlem32  34928  cnambfre  34944  itg2addnclem2  34948  ftc1anclem1  34971  ftc1anclem6  34976  lkrval  36228  pw2f1o2val  39642  aomclem8  39667  pwfi2f1o  39702  trclimalb2  40077  frege131d  40115  colleq12d  40595  dirkercncflem2  42396  issmflem  43011  smfpimioo  43069  smfpimcc  43089  smfsuplem2  43093