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

Theorem imaeq1d 5672
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 5668 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cima 5311
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3an 1102  df-tru 1641  df-ex 1860  df-nf 1865  df-sb 2063  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-rab 3104  df-v 3392  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-nul 4114  df-if 4277  df-sn 4368  df-pr 4370  df-op 4374  df-br 4841  df-opab 4903  df-cnv 5316  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321
This theorem is referenced by:  imaeq12d  5674  nfimad  5682  csbrn  5804  f1imacnv  6366  foimacnv  6367  fimacnvinrn  6567  seqomeq12  7782  ssenen  8370  fipreima  8508  oieq1  8653  oieq2  8654  dfac12lem1  9247  dfac12r  9250  fpwwe2cbv  9734  fpwwe2lem2  9736  fpwwecbv  9748  fpwwelem  9749  seqeq1  13023  seqeq2  13024  seqeq3  13025  1arith  15844  vdwmc  15895  vdwnnlem1  15912  ramub2  15931  rami  15932  imasless  16401  gsumvalx  17471  eqglact  17843  psgnunilem1  18110  psrbag  19569  psrbaglefi  19577  evpmss  20135  psgnevpmb  20136  frlmup3  20345  iscn  21249  ptbasfi  21594  ptval2  21614  ptrescn  21652  xkoptsub  21667  qtopval  21708  cmphaushmeo  21813  ptcmpg  22070  restutopopn  22251  prdsxmslem2  22543  metuval  22563  nghmfval  22735  isnghm  22736  ismbf1  23601  ismbf  23605  mbfconst  23610  mbfres2  23622  cncombf  23635  isi1f  23651  itg1val  23660  deg1val  24066  fta1glem2  24136  fta1g  24137  fta1b  24139  dgrval  24194  dgrlem  24195  coeidlem  24203  coe11  24219  fta1lem  24272  fta1  24273  vieta1lem2  24276  vieta1  24277  taylthlem2  24338  areaval  24901  sqff1o  25118  nlfnval  29065  xppreima2  29774  ofpreima  29789  fpwrelmapffslem  29831  xrhval  30384  indf1ofs  30410  ismbfm  30636  mbfmcst  30643  issibf  30717  sitgfval  30725  eulerpartlemelr  30741  eulerpartleme  30747  eulerpartlemo  30749  eulerpartlemt0  30753  eulerpartlemt  30755  eulerpartlemr  30758  eulerpartlemgf  30763  eulerpartlemgs2  30764  eulerpartlemn  30765  eulerpart  30766  ballotlemscr  30902  ballotlemrv  30903  ballotlemrinv0  30916  iscvm  31561  cvmliftmolem1  31583  cvmlift2lem9a  31605  cvmlift2lem9  31613  msrfval  31754  ismfs  31766  mthmval  31792  poimirlem4  33723  poimirlem5  33724  poimirlem6  33725  poimirlem7  33726  poimirlem8  33727  poimirlem10  33729  poimirlem11  33730  poimirlem12  33731  poimirlem13  33732  poimirlem14  33733  poimirlem15  33734  poimirlem16  33735  poimirlem17  33736  poimirlem18  33737  poimirlem19  33738  poimirlem20  33739  poimirlem21  33740  poimirlem22  33741  poimirlem26  33745  poimirlem27  33746  poimirlem32  33751  cnambfre  33767  itg2addnclem2  33771  ftc1anclem1  33794  ftc1anclem6  33799  lkrval  34865  pw2f1o2val  38104  aomclem8  38129  pwfi2f1o  38164  trclimalb2  38515  frege131d  38553  dirkercncflem2  40797  issmflem  41415  smfpimioo  41473  smfpimcc  41493  smfsuplem2  41497
  Copyright terms: Public domain W3C validator