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

Theorem imaeq1d 5922
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 5918 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1528  cima 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2793
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-3an 1081  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-rab 3147  df-v 3497  df-dif 3938  df-un 3940  df-in 3942  df-ss 3951  df-nul 4291  df-if 4466  df-sn 4560  df-pr 4562  df-op 4566  df-br 5059  df-opab 5121  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562
This theorem is referenced by:  imaeq12d  5924  nfimad  5932  csbrn  6054  f1imacnv  6625  foimacnv  6626  fimacnvinrn  6833  seqomeq12  8081  ssenen  8680  fipreima  8819  oieq1  8965  oieq2  8966  dfac12lem1  9558  dfac12r  9561  fpwwe2cbv  10041  fpwwe2lem2  10043  fpwwecbv  10055  fpwwelem  10056  seqeq1  13362  seqeq2  13363  seqeq3  13364  1arith  16253  vdwmc  16304  vdwnnlem1  16321  ramub2  16340  rami  16341  imasless  16803  gsumvalx  17876  eqglact  18271  psgnunilem1  18552  psrbag  20074  psrbaglefi  20082  evpmss  20660  psgnevpmb  20661  frlmup3  20874  iscn  21773  ptbasfi  22119  ptval2  22139  ptrescn  22177  xkoptsub  22192  qtopval  22233  cmphaushmeo  22338  ptcmpg  22595  restutopopn  22776  prdsxmslem2  23068  metuval  23088  nghmfval  23260  isnghm  23261  ismbf1  24154  ismbf  24158  mbfconst  24163  mbfres2  24175  cncombf  24188  isi1f  24204  itg1val  24213  deg1val  24619  fta1glem2  24689  fta1g  24690  fta1b  24692  dgrval  24747  dgrlem  24748  coeidlem  24756  coe11  24772  fta1lem  24825  fta1  24826  vieta1lem2  24829  vieta1  24830  taylthlem2  24891  areaval  25470  sqff1o  25687  nlfnval  29586  xppreima2  30324  ofpreima  30339  fpwrelmapffslem  30395  evpmval  30715  altgnsg  30719  xrhval  31159  indf1ofs  31185  ismbfm  31410  mbfmcst  31417  issibf  31491  sitgfval  31499  eulerpartlemelr  31515  eulerpartleme  31521  eulerpartlemo  31523  eulerpartlemt0  31527  eulerpartlemt  31529  eulerpartlemr  31532  eulerpartlemgf  31537  eulerpartlemgs2  31538  eulerpartlemn  31539  eulerpart  31540  ballotlemscr  31676  ballotlemrv  31677  ballotlemrinv0  31690  iscvm  32404  cvmliftmolem1  32426  cvmlift2lem9a  32448  cvmlift2lem9  32456  msrfval  32682  ismfs  32694  mthmval  32720  bj-imdirval2  34366  poimirlem4  34778  poimirlem5  34779  poimirlem6  34780  poimirlem7  34781  poimirlem8  34782  poimirlem10  34784  poimirlem11  34785  poimirlem12  34786  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem18  34792  poimirlem19  34793  poimirlem20  34794  poimirlem21  34795  poimirlem22  34796  poimirlem26  34800  poimirlem27  34801  poimirlem32  34806  cnambfre  34822  itg2addnclem2  34826  ftc1anclem1  34849  ftc1anclem6  34854  lkrval  36106  pw2f1o2val  39516  aomclem8  39541  pwfi2f1o  39576  trclimalb2  39951  frege131d  39989  colleq12d  40469  dirkercncflem2  42270  issmflem  42885  smfpimioo  42943  smfpimcc  42963  smfsuplem2  42967
  Copyright terms: Public domain W3C validator