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

Theorem imaeq1d 5623
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 5619 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1632  cima 5269
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1871  ax-4 1886  ax-5 1988  ax-6 2054  ax-7 2090  ax-9 2148  ax-10 2168  ax-11 2183  ax-12 2196  ax-13 2391  ax-ext 2740
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1635  df-ex 1854  df-nf 1859  df-sb 2047  df-clab 2747  df-cleq 2753  df-clel 2756  df-nfc 2891  df-rab 3059  df-v 3342  df-dif 3718  df-un 3720  df-in 3722  df-ss 3729  df-nul 4059  df-if 4231  df-sn 4322  df-pr 4324  df-op 4328  df-br 4805  df-opab 4865  df-cnv 5274  df-dm 5276  df-rn 5277  df-res 5278  df-ima 5279
This theorem is referenced by:  imaeq12d  5625  nfimad  5633  csbrn  5754  f1imacnv  6315  foimacnv  6316  fimacnvinrn  6512  seqomeq12  7719  ssenen  8301  fipreima  8439  oieq1  8584  oieq2  8585  dfac12lem1  9177  dfac12r  9180  fpwwe2cbv  9664  fpwwe2lem2  9666  fpwwecbv  9678  fpwwelem  9679  seqeq1  13018  seqeq2  13019  seqeq3  13020  1arith  15853  vdwmc  15904  vdwnnlem1  15921  ramub2  15940  rami  15941  imasless  16422  gsumvalx  17491  eqglact  17866  psgnunilem1  18133  psrbag  19586  psrbaglefi  19594  evpmss  20154  psgnevpmb  20155  frlmup3  20361  iscn  21261  ptbasfi  21606  ptval2  21626  ptrescn  21664  xkoptsub  21679  qtopval  21720  cmphaushmeo  21825  ptcmpg  22082  restutopopn  22263  prdsxmslem2  22555  metuval  22575  nghmfval  22747  isnghm  22748  ismbf1  23612  ismbf  23616  mbfconst  23621  mbfres2  23631  cncombf  23644  isi1f  23660  itg1val  23669  deg1val  24075  fta1glem2  24145  fta1g  24146  fta1b  24148  dgrval  24203  dgrlem  24204  coeidlem  24212  coe11  24228  fta1lem  24281  fta1  24282  vieta1lem2  24285  vieta1  24286  taylthlem2  24347  areaval  24911  sqff1o  25128  nlfnval  29070  xppreima2  29780  ofpreima  29795  fpwrelmapffslem  29837  xrhval  30392  indf1ofs  30418  ismbfm  30644  mbfmcst  30651  issibf  30725  sitgfval  30733  eulerpartlemelr  30749  eulerpartleme  30755  eulerpartlemo  30757  eulerpartlemt0  30761  eulerpartlemt  30763  eulerpartlemr  30766  eulerpartlemgf  30771  eulerpartlemgs2  30772  eulerpartlemn  30773  eulerpart  30774  ballotlemscr  30910  ballotlemrv  30911  ballotlemrinv0  30924  iscvm  31569  cvmliftmolem1  31591  cvmlift2lem9a  31613  cvmlift2lem9  31621  msrfval  31762  ismfs  31774  mthmval  31800  poimirlem4  33744  poimirlem5  33745  poimirlem6  33746  poimirlem7  33747  poimirlem8  33748  poimirlem10  33750  poimirlem11  33751  poimirlem12  33752  poimirlem13  33753  poimirlem14  33754  poimirlem15  33755  poimirlem16  33756  poimirlem17  33757  poimirlem18  33758  poimirlem19  33759  poimirlem20  33760  poimirlem21  33761  poimirlem22  33762  poimirlem26  33766  poimirlem27  33767  poimirlem32  33772  cnambfre  33789  itg2addnclem2  33793  ftc1anclem1  33816  ftc1anclem6  33821  lkrval  34896  pw2f1o2val  38126  aomclem8  38151  pwfi2f1o  38186  trclimalb2  38538  frege131d  38576  dirkercncflem2  40842  issmflem  41460  smfpimioo  41518  smfpimcc  41538  smfsuplem2  41542
  Copyright terms: Public domain W3C validator