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

Theorem imaeq1d 5371
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 5367 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  cima 5031
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-3an 1032  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-rab 2904  df-v 3174  df-dif 3542  df-un 3544  df-in 3546  df-ss 3553  df-nul 3874  df-if 4036  df-sn 4125  df-pr 4127  df-op 4131  df-br 4578  df-opab 4638  df-cnv 5036  df-dm 5038  df-rn 5039  df-res 5040  df-ima 5041
This theorem is referenced by:  imaeq12d  5373  nfimad  5381  csbrn  5500  f1imacnv  6051  foimacnv  6052  fimacnvinrn  6241  seqomeq12  7414  ssenen  7997  fipreima  8133  oieq1  8278  oieq2  8279  dfac12lem1  8826  dfac12r  8829  fpwwe2cbv  9309  fpwwe2lem2  9311  fpwwecbv  9323  fpwwelem  9324  seqeq1  12624  seqeq2  12625  seqeq3  12626  1arith  15418  vdwmc  15469  vdwnnlem1  15486  ramub2  15505  rami  15506  imasless  15972  gsumvalx  17042  eqglact  17417  psgnunilem1  17685  psrbag  19134  psrbaglefi  19142  evpmss  19699  psgnevpmb  19700  frlmup3  19906  iscn  20797  ptbasfi  21142  ptval2  21162  ptrescn  21200  xkoptsub  21215  qtopval  21256  cmphaushmeo  21361  ptcmpg  21619  restutopopn  21800  prdsxmslem2  22092  metuval  22112  nghmfval  22284  isnghm  22285  ismbf1  23144  ismbf  23148  mbfconst  23153  mbfres2  23163  cncombf  23176  isi1f  23192  itg1val  23201  deg1val  23605  fta1glem2  23675  fta1g  23676  fta1b  23678  dgrval  23733  dgrlem  23734  coeidlem  23742  coe11  23758  fta1lem  23811  fta1  23812  vieta1lem2  23815  vieta1  23816  taylthlem2  23877  areaval  24436  sqff1o  24653  nlfnval  27958  xppreima2  28664  ofpreima  28682  fpwrelmapffslem  28729  xrhval  29224  indf1ofs  29249  ismbfm  29475  mbfmcst  29482  issibf  29556  sitgfval  29564  eulerpartlemelr  29580  eulerpartleme  29586  eulerpartlemo  29588  eulerpartlemt0  29592  eulerpartlemt  29594  eulerpartlemr  29597  eulerpartlemgf  29602  eulerpartlemgs2  29603  eulerpartlemn  29604  eulerpart  29605  ballotlemscr  29741  ballotlemrv  29742  ballotlemrinv0  29755  iscvm  30329  cvmliftmolem1  30351  cvmlift2lem9a  30373  cvmlift2lem9  30381  msrfval  30522  ismfs  30534  mthmval  30560  poimirlem4  32407  poimirlem5  32408  poimirlem6  32409  poimirlem7  32410  poimirlem8  32411  poimirlem10  32413  poimirlem11  32414  poimirlem12  32415  poimirlem13  32416  poimirlem14  32417  poimirlem15  32418  poimirlem16  32419  poimirlem17  32420  poimirlem18  32421  poimirlem19  32422  poimirlem20  32423  poimirlem21  32424  poimirlem22  32425  poimirlem26  32429  poimirlem27  32430  poimirlem32  32435  cnambfre  32452  itg2addnclem2  32456  ftc1anclem1  32479  ftc1anclem6  32484  lkrval  33217  pw2f1o2val  36448  aomclem8  36473  pwfi2f1o  36508  trclimalb2  36861  frege131d  36899  dirkercncflem2  38821  issmflem  39437  smfpimioo  39496
  Copyright terms: Public domain W3C validator