Theorem imaeq1d 5930

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 5926	. 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-cnv 5565  df-dm 5567  df-rn 5568  df-res 5569  df-ima 5570

This theorem is referenced by:  imaeq12d  5932  nfimad  5940  csbrn  6062  f1imacnv  6633  foimacnv  6634  fimacnvinrn  6842  seqomeq12  8092  ssenen  8693  fipreima  8832  oieq1  8978  oieq2  8979  dfac12lem1  9571  dfac12r  9574  fpwwe2cbv  10054  fpwwe2lem2  10056  fpwwecbv  10068  fpwwelem  10069  seqeq1  13375  seqeq2  13376  seqeq3  13377  1arith  16265  vdwmc  16316  vdwnnlem1  16333  ramub2  16352  rami  16353  imasless  16815  gsumvalx  17888  eqglact  18333  psgnunilem1  18623  psrbag  20146  psrbaglefi  20154  evpmss  20732  psgnevpmb  20733  frlmup3  20946  iscn  21845  ptbasfi  22191  ptval2  22211  ptrescn  22249  xkoptsub  22264  qtopval  22305  cmphaushmeo  22410  ptcmpg  22667  restutopopn  22849  prdsxmslem2  23141  metuval  23161  nghmfval  23333  isnghm  23334  ismbf1  24227  ismbf  24231  mbfconst  24236  mbfres2  24248  cncombf  24261  isi1f  24277  itg1val  24286  deg1val  24692  fta1glem2  24762  fta1g  24763  fta1b  24765  dgrval  24820  dgrlem  24821  coeidlem  24829  coe11  24845  fta1lem  24898  fta1  24899  vieta1lem2  24902  vieta1  24903  taylthlem2  24964  areaval  25544  sqff1o  25761  nlfnval  29660  xppreima2  30397  ofpreima  30412  fpwrelmapffslem  30470  evpmval  30789  altgnsg  30793  xrhval  31261  indf1ofs  31287  ismbfm  31512  mbfmcst  31519  issibf  31593  sitgfval  31601  eulerpartlemelr  31617  eulerpartleme  31623  eulerpartlemo  31625  eulerpartlemt0  31629  eulerpartlemt  31631  eulerpartlemr  31634  eulerpartlemgf  31639  eulerpartlemgs2  31640  eulerpartlemn  31641  eulerpart  31642  ballotlemscr  31778  ballotlemrv  31779  ballotlemrinv0  31792  iscvm  32508  cvmliftmolem1  32530  cvmlift2lem9a  32552  cvmlift2lem9  32560  msrfval  32786  ismfs  32798  mthmval  32824  bj-imdirval2  34475  poimirlem4  34898  poimirlem5  34899  poimirlem6  34900  poimirlem7  34901  poimirlem8  34902  poimirlem10  34904  poimirlem11  34905  poimirlem12  34906  poimirlem13  34907  poimirlem14  34908  poimirlem15  34909  poimirlem16  34910  poimirlem17  34911  poimirlem18  34912  poimirlem19  34913  poimirlem20  34914  poimirlem21  34915  poimirlem22  34916  poimirlem26  34920  poimirlem27  34921  poimirlem32  34926  cnambfre  34942  itg2addnclem2  34946  ftc1anclem1  34969  ftc1anclem6  34974  lkrval  36226  pw2f1o2val  39643  aomclem8  39668  pwfi2f1o  39703  trclimalb2  40078  frege131d  40116  colleq12d  40596  dirkercncflem2  42396  issmflem  43011  smfpimioo  43069  smfpimcc  43089  smfsuplem2  43093