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

Theorem imaeq2d 5690
Description: Equality theorem for image. (Contributed by FL, 15-Dec-2006.)
Hypothesis
Ref Expression
imaeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
imaeq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem imaeq2d
StepHypRef Expression
1 imaeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 imaeq2 5686 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  cima 5327
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
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 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-rab 3116  df-v 3404  df-dif 3783  df-un 3785  df-in 3787  df-ss 3794  df-nul 4128  df-if 4291  df-sn 4382  df-pr 4384  df-op 4388  df-br 4856  df-opab 4918  df-xp 5330  df-cnv 5332  df-dm 5334  df-rn 5335  df-res 5336  df-ima 5337
This theorem is referenced by:  imaeq12d  5691  nfimad  5699  csbima12  5707  elimasng  5715  elimasni  5716  inisegn0  5721  csbrn  5821  ressn  5899  foima  6346  f1imacnv  6379  dffv3  6414  fvco2  6504  fimacnvinrn2  6581  fsn2  6636  funfvima3  6730  isofrlem  6824  isoselem  6825  fnexALT  7372  curry1  7513  curry2  7516  fparlem3  7523  fparlem4  7524  suppsnop  7553  ressuppssdif  7560  imacosupp  7580  eceq1  8027  uniqs2  8054  ecinxp  8067  mapsnd  8144  sbthlem2  8320  sbth  8329  phplem4  8391  php3  8395  marypha1lem  8588  cantnfp1lem3  8834  tcrank  9004  fin4en1  9426  fin1a2lem7  9523  hsmexlem4  9546  hsmexlem5  9547  fpwwe2cbv  9747  fpwwe2lem3  9750  fpwwe2lem13  9759  fpwwecbv  9761  canth4  9764  frnnn0fsupp  11636  resunimafz0  13466  limsupgval  14450  isercoll  14641  vdwlem1  15922  vdwlem6  15927  vdwlem7  15928  vdwlem8  15929  vdwlem12  15933  vdwlem13  15934  vdwnn  15939  0ram  15961  ramz2  15965  isacs1i  16542  acsficl  17396  gsumvalx  17495  gsumpropd  17497  gsumpropd2lem  17498  gsumress  17501  efgrelexlema  18383  gsumval3a  18525  gsumval3lem1  18527  gsum2dlem2  18591  gsum2d2  18594  dprddisj  18630  dprdf1o  18653  dprdsn  18657  dprd2dlem2  18661  dprd2dlem1  18662  dprd2da  18663  dprd2db  18664  dmdprdsplit2lem  18666  dpjfval  18676  coe1mul2lem2  19866  frlmup3  20370  islindf  20382  islindf2  20384  lindfind  20386  f1lindf  20392  lmimlbs  20406  subbascn  21293  cncls2  21312  cncls  21313  cnntr  21314  cnpresti  21327  cnprest  21328  cnt1  21389  cnhaus  21393  cncmp  21430  cnconn  21460  1stcfb  21483  xkoccn  21657  ptrescn  21677  xkococnlem  21697  qtopeu  21754  qtoprest  21755  kqdisj  21770  kqcldsat  21771  ordthmeolem  21839  fmfnfmlem4  21995  ustuqtoplem  22277  utopsnneiplem  22285  utopsnneip  22286  ucncn  22323  metustto  22592  metustexhalf  22595  metustfbas  22596  cfilucfil  22598  metuust  22599  cfilucfil2  22600  metuel  22603  metuel2  22604  psmetutop  22606  restmetu  22609  metucn  22610  pi1addval  23081  iscph  23203  cphsscph  23283  uniioombllem3  23589  dyadmbl  23604  mbfima  23634  mbfimaicc  23635  mbfimasn  23636  ismbfd  23643  ismbf2d  23644  ismbf3d  23658  mbfimaopnlem  23659  i1fd  23685  i1f1  23694  itg11  23695  i1faddlem  23697  i1fmullem  23698  i1fadd  23699  itg1addlem3  23702  itg1mulc  23708  itg2gt0  23764  limcnlp  23879  ellimc3  23880  limcflf  23882  limciun  23895  mdegval  24060  mdeg0  24067  mdegvsca  24073  mdegpropd  24081  deg1val  24093  ig1pval  24169  coeeu  24218  coeeq  24220  pserulm  24413  areambl  24922  pthdlem2  26915  eupth2lem3  27432  eupth2  27435  issh  28416  isch  28430  shsval  28522  sspreima  29797  dfcnv2  29826  gsummpt2co  30128  smatrcl  30210  locfinreflem  30255  zrhunitpreima  30370  mbfmco2  30675  sibfima  30748  sibfof  30750  eulerpartlemgv  30783  eulerpartlemn  30791  eulerpart  30792  orvcval4  30870  orvcelval  30878  orvcelel  30879  ballotlemscr  30928  erdszelem3  31520  erdsze  31529  cvmliftlem3  31614  cvmliftlem7  31618  cvmlift2lem9a  31630  msrval  31780  mvtinf  31797  mclsval  31805  mclsax  31811  mthmpps  31824  opelco3  32020  scutval  32254  madeval  32278  funpartlem  32392  tailval  32711  csbpredg  33508  ptrest  33740  poimirlem1  33742  poimirlem2  33743  poimirlem3  33744  poimirlem4  33745  poimirlem5  33746  poimirlem6  33747  poimirlem7  33748  poimirlem9  33750  poimirlem10  33751  poimirlem11  33752  poimirlem12  33753  poimirlem13  33754  poimirlem14  33755  poimirlem15  33756  poimirlem16  33757  poimirlem17  33758  poimirlem19  33760  poimirlem20  33761  poimirlem22  33763  poimirlem23  33764  poimirlem24  33765  poimirlem25  33766  poimirlem26  33767  poimirlem27  33768  poimirlem28  33769  poimirlem29  33770  poimirlem31  33772  poimirlem32  33773  mblfinlem2  33779  volsupnfl  33786  itg2addnclem2  33793  sstotbnd2  33903  ismtyhmeolem  33933  grpokerinj  34022  lkrfval  34886  dnnumch3lem  38135  aomclem8  38150  pwfi2f1o  38185  cytpval  38306  frege97d  38562  frege109d  38567  frege131d  38574  nzprmdif  39036  wessf1ornlem  39878  limsuplesup  40429  limsupvaluz  40438  limsuplt2  40483  limsupge  40491  liminfgval  40492  liminfval2  40498  liminflelimsuplem  40505  liminflelimsup  40506  preimaioomnf  41429  afv2co2  41864  imarnf1pr  41890
  Copyright terms: Public domain W3C validator