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

Theorem imaeq2d 5923
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 5919 . 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-xp 5555  df-cnv 5557  df-dm 5559  df-rn 5560  df-res 5561  df-ima 5562
This theorem is referenced by:  imaeq12d  5924  nfimad  5932  csbima12  5941  elimasng  5949  elimasni  5950  inisegn0  5955  csbrn  6054  ressn  6130  foima  6589  f1imacnv  6625  dffv3  6660  fvco2  6752  fimacnvinrn2  6834  fsn2  6891  funfvima3  6989  isofrlem  7082  isoselem  7083  fnexALT  7643  curry1  7790  curry2  7793  fparlem3  7800  fparlem4  7801  suppsnop  7835  ressuppssdif  7842  suppco  7861  imacosupp  7865  imacosuppOLD  7866  eceq1  8317  uniqs2  8349  ecinxp  8362  mapsnd  8439  sbthlem2  8617  sbth  8626  phplem4  8688  php3  8692  marypha1lem  8886  cantnfp1lem3  9132  tcrank  9302  fin4en1  9720  fin1a2lem7  9817  hsmexlem4  9840  hsmexlem5  9841  fpwwe2cbv  10041  fpwwe2lem3  10044  fpwwe2lem13  10053  fpwwecbv  10055  canth4  10058  frnnn0fsupp  11943  resunimafz0  13793  limsupgval  14823  isercoll  15014  vdwlem1  16307  vdwlem6  16312  vdwlem7  16313  vdwlem8  16314  vdwlem12  16318  vdwlem13  16319  vdwnn  16324  0ram  16346  ramz2  16350  isacs1i  16918  acsficl  17771  gsumvalx  17876  gsumpropd  17878  gsumpropd2lem  17879  gsumress  17882  efgrelexlema  18806  gsumval3a  18954  gsumval3lem1  18956  gsum2dlem2  19022  gsum2d2  19025  dprddisj  19062  dprdf1o  19085  dprdsn  19089  dprd2dlem2  19093  dprd2dlem1  19094  dprd2da  19095  dprd2db  19096  dmdprdsplit2lem  19098  dpjfval  19108  coe1mul2lem2  20366  frlmup3  20874  islindf  20886  islindf2  20888  lindfind  20890  f1lindf  20896  lmimlbs  20910  subbascn  21792  cncls2  21811  cncls  21812  cnntr  21813  cnpresti  21826  cnprest  21827  cnt1  21888  cnhaus  21892  cncmp  21930  cnconn  21960  1stcfb  21983  xkoccn  22157  ptrescn  22177  xkococnlem  22197  qtopeu  22254  qtoprest  22255  kqdisj  22270  kqcldsat  22271  ordthmeolem  22339  fmfnfmlem4  22495  ustuqtoplem  22777  utopsnneiplem  22785  utopsnneip  22786  ucncn  22823  metustto  23092  metustexhalf  23095  metustfbas  23096  cfilucfil  23098  metuust  23099  cfilucfil2  23100  metuel  23103  metuel2  23104  psmetutop  23106  restmetu  23109  metucn  23110  pi1addval  23581  iscph  23703  cphsscph  23783  uniioombllem3  24115  dyadmbl  24130  mbfima  24160  mbfimaicc  24161  mbfimasn  24162  ismbfd  24169  ismbf2d  24170  ismbf3d  24184  mbfimaopnlem  24185  i1fd  24211  i1f1  24220  itg11  24221  i1faddlem  24223  i1fmullem  24224  i1fadd  24225  itg1addlem3  24228  itg1mulc  24234  itg2gt0  24290  limcnlp  24405  ellimc3  24406  limcflf  24408  limciun  24421  mdegval  24586  mdeg0  24593  mdegvsca  24599  mdegpropd  24607  deg1val  24619  ig1pval  24695  coeeu  24744  coeeq  24746  pserulm  24939  areambl  25464  pthdlem2  27477  eupth2lem3  27943  eupth2  27946  issh  28913  isch  28927  shsval  29017  sspreima  30321  fnpreimac  30345  dfcnv2  30351  s2rn  30548  s3rn  30550  swrdrndisj  30559  gsummpt2co  30614  cycpmco2rn  30695  dimval  30901  dimvalfi  30902  extdgval  30944  smatrcl  30961  locfinreflem  31004  zrhunitpreima  31119  mbfmco2  31423  sibfima  31496  sibfof  31498  eulerpartlemgv  31531  eulerpartlemn  31539  eulerpart  31540  orvcval4  31618  orvcelval  31626  orvcelel  31627  ballotlemscr  31676  f1resfz0f1d  32259  pthhashvtx  32272  erdszelem3  32338  erdsze  32347  cvmliftlem3  32432  cvmliftlem7  32436  cvmlift2lem9a  32448  msrval  32683  mvtinf  32700  mclsval  32708  mclsax  32714  mthmpps  32727  opelco3  32916  scutval  33163  madeval  33187  funpartlem  33301  tailval  33619  csbpredg  34490  ptrest  34773  poimirlem1  34775  poimirlem2  34776  poimirlem3  34777  poimirlem4  34778  poimirlem5  34779  poimirlem6  34780  poimirlem7  34781  poimirlem9  34783  poimirlem10  34784  poimirlem11  34785  poimirlem12  34786  poimirlem13  34787  poimirlem14  34788  poimirlem15  34789  poimirlem16  34790  poimirlem17  34791  poimirlem19  34793  poimirlem20  34794  poimirlem22  34796  poimirlem23  34797  poimirlem24  34798  poimirlem25  34799  poimirlem26  34800  poimirlem27  34801  poimirlem28  34802  poimirlem29  34803  poimirlem31  34805  poimirlem32  34806  mblfinlem2  34812  volsupnfl  34819  itg2addnclem2  34826  sstotbnd2  34935  ismtyhmeolem  34965  grpokerinj  35054  lkrfval  36105  dnnumch3lem  39526  aomclem8  39541  pwfi2f1o  39576  cytpval  39689  frege97d  39977  frege109d  39982  frege131d  39989  nzprmdif  40531  wessf1ornlem  41325  limsuplesup  41860  limsupvaluz  41869  limsuplt2  41914  limsupge  41922  liminfgval  41923  liminfval2  41929  liminflelimsuplem  41936  liminflelimsup  41937  preimaioomnf  42878  afv2co2  43337  imarnf1pr  43362  isomgr  43835  isomushgr  43838  isomgrsym  43848  isomgrtrlem  43850
  Copyright terms: Public domain W3C validator