MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imaeq1d Structured version   Visualization version   GIF version

Theorem imaeq1d 5915
Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
Hypothesis
Ref Expression
imaeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
imaeq1d (𝜑 → (𝐴𝐶) = (𝐵𝐶))

Proof of Theorem imaeq1d
StepHypRef Expression
1 imaeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 imaeq1 5911 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cima 5545
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 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2179  ax-ext 2796
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 2071  df-clab 2803  df-cleq 2817  df-clel 2896  df-nfc 2964  df-rab 3142  df-v 3482  df-un 3924  df-in 3926  df-ss 3936  df-sn 4551  df-pr 4553  df-op 4557  df-br 5053  df-opab 5115  df-cnv 5550  df-dm 5552  df-rn 5553  df-res 5554  df-ima 5555
This theorem is referenced by:  imaeq12d  5917  nfimad  5925  csbrn  6047  f1imacnv  6622  foimacnv  6623  fimacnvinrn  6831  seqomeq12  8086  ssenen  8688  fipreima  8827  oieq1  8973  oieq2  8974  dfac12lem1  9567  dfac12r  9570  fpwwe2cbv  10050  fpwwe2lem2  10052  fpwwecbv  10064  fpwwelem  10065  seqeq1  13376  seqeq2  13377  seqeq3  13378  1arith  16261  vdwmc  16312  vdwnnlem1  16329  ramub2  16348  rami  16349  imasless  16813  gsumvalx  17886  eqglact  18331  psgnunilem1  18621  psrbag  20144  psrbaglefi  20152  evpmss  20730  psgnevpmb  20731  frlmup3  20944  iscn  21843  ptbasfi  22189  ptval2  22209  ptrescn  22247  xkoptsub  22262  qtopval  22303  cmphaushmeo  22408  ptcmpg  22665  restutopopn  22847  prdsxmslem2  23139  metuval  23159  nghmfval  23331  isnghm  23332  ismbf1  24231  ismbf  24235  mbfconst  24240  mbfres2  24252  cncombf  24265  isi1f  24281  itg1val  24290  deg1val  24700  fta1glem2  24770  fta1g  24771  fta1b  24773  dgrval  24828  dgrlem  24829  coeidlem  24837  coe11  24853  fta1lem  24906  fta1  24907  vieta1lem2  24910  vieta1  24911  taylthlem2  24972  areaval  25553  sqff1o  25770  nlfnval  29667  xppreima2  30406  ofpreima  30421  fpwrelmapffslem  30479  evpmval  30819  altgnsg  30823  xrhval  31316  indf1ofs  31342  ismbfm  31567  mbfmcst  31574  issibf  31648  sitgfval  31656  eulerpartlemelr  31672  eulerpartleme  31678  eulerpartlemo  31680  eulerpartlemt0  31684  eulerpartlemt  31686  eulerpartlemr  31689  eulerpartlemgf  31694  eulerpartlemgs2  31695  eulerpartlemn  31696  eulerpart  31697  ballotlemscr  31833  ballotlemrv  31834  ballotlemrinv0  31847  iscvm  32563  cvmliftmolem1  32585  cvmlift2lem9a  32607  cvmlift2lem9  32615  msrfval  32841  ismfs  32853  mthmval  32879  bj-imdirval2  34543  bj-iminvval2  34554  poimirlem4  35006  poimirlem5  35007  poimirlem6  35008  poimirlem7  35009  poimirlem8  35010  poimirlem10  35012  poimirlem11  35013  poimirlem12  35014  poimirlem13  35015  poimirlem14  35016  poimirlem15  35017  poimirlem16  35018  poimirlem17  35019  poimirlem18  35020  poimirlem19  35021  poimirlem20  35022  poimirlem21  35023  poimirlem22  35024  poimirlem26  35028  poimirlem27  35029  poimirlem32  35034  cnambfre  35050  itg2addnclem2  35054  ftc1anclem1  35075  ftc1anclem6  35080  lkrval  36329  pw2f1o2val  39896  aomclem8  39921  pwfi2f1o  39956  trclimalb2  40343  frege131d  40381  colleq12d  40881  dirkercncflem2  42672  issmflem  43287  smfpimioo  43345  smfpimcc  43365  smfsuplem2  43369
  Copyright terms: Public domain W3C validator