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

Theorem imaeq1d 5575
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 5571 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1596  cima 5221
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1835  ax-4 1850  ax-5 1952  ax-6 2018  ax-7 2054  ax-9 2112  ax-10 2132  ax-11 2147  ax-12 2160  ax-13 2355  ax-ext 2704
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-3an 1074  df-tru 1599  df-ex 1818  df-nf 1823  df-sb 2011  df-clab 2711  df-cleq 2717  df-clel 2720  df-nfc 2855  df-rab 3023  df-v 3306  df-dif 3683  df-un 3685  df-in 3687  df-ss 3694  df-nul 4024  df-if 4195  df-sn 4286  df-pr 4288  df-op 4292  df-br 4761  df-opab 4821  df-cnv 5226  df-dm 5228  df-rn 5229  df-res 5230  df-ima 5231
This theorem is referenced by:  imaeq12d  5577  nfimad  5585  csbrn  5706  f1imacnv  6266  foimacnv  6267  fimacnvinrn  6463  seqomeq12  7669  ssenen  8250  fipreima  8388  oieq1  8533  oieq2  8534  dfac12lem1  9078  dfac12r  9081  fpwwe2cbv  9565  fpwwe2lem2  9567  fpwwecbv  9579  fpwwelem  9580  seqeq1  12919  seqeq2  12920  seqeq3  12921  1arith  15754  vdwmc  15805  vdwnnlem1  15822  ramub2  15841  rami  15842  imasless  16323  gsumvalx  17392  eqglact  17767  psgnunilem1  18034  psrbag  19487  psrbaglefi  19495  evpmss  20055  psgnevpmb  20056  frlmup3  20262  iscn  21162  ptbasfi  21507  ptval2  21527  ptrescn  21565  xkoptsub  21580  qtopval  21621  cmphaushmeo  21726  ptcmpg  21983  restutopopn  22164  prdsxmslem2  22456  metuval  22476  nghmfval  22648  isnghm  22649  ismbf1  23513  ismbf  23517  mbfconst  23522  mbfres2  23532  cncombf  23545  isi1f  23561  itg1val  23570  deg1val  23976  fta1glem2  24046  fta1g  24047  fta1b  24049  dgrval  24104  dgrlem  24105  coeidlem  24113  coe11  24129  fta1lem  24182  fta1  24183  vieta1lem2  24186  vieta1  24187  taylthlem2  24248  areaval  24811  sqff1o  25028  nlfnval  28970  xppreima2  29680  ofpreima  29695  fpwrelmapffslem  29737  xrhval  30292  indf1ofs  30318  ismbfm  30544  mbfmcst  30551  issibf  30625  sitgfval  30633  eulerpartlemelr  30649  eulerpartleme  30655  eulerpartlemo  30657  eulerpartlemt0  30661  eulerpartlemt  30663  eulerpartlemr  30666  eulerpartlemgf  30671  eulerpartlemgs2  30672  eulerpartlemn  30673  eulerpart  30674  ballotlemscr  30810  ballotlemrv  30811  ballotlemrinv0  30824  iscvm  31469  cvmliftmolem1  31491  cvmlift2lem9a  31513  cvmlift2lem9  31521  msrfval  31662  ismfs  31674  mthmval  31700  poimirlem4  33645  poimirlem5  33646  poimirlem6  33647  poimirlem7  33648  poimirlem8  33649  poimirlem10  33651  poimirlem11  33652  poimirlem12  33653  poimirlem13  33654  poimirlem14  33655  poimirlem15  33656  poimirlem16  33657  poimirlem17  33658  poimirlem18  33659  poimirlem19  33660  poimirlem20  33661  poimirlem21  33662  poimirlem22  33663  poimirlem26  33667  poimirlem27  33668  poimirlem32  33673  cnambfre  33690  itg2addnclem2  33694  ftc1anclem1  33717  ftc1anclem6  33722  lkrval  34795  pw2f1o2val  38025  aomclem8  38050  pwfi2f1o  38085  trclimalb2  38437  frege131d  38475  dirkercncflem2  40741  issmflem  41359  smfpimioo  41417  smfpimcc  41437  smfsuplem2  41441
  Copyright terms: Public domain W3C validator