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

Theorem imaeq2d 5896
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 5892 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1538  cima 5522
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2113  ax-9 2121  ax-10 2142  ax-11 2158  ax-12 2175  ax-ext 2770
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-3an 1086  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2070  df-clab 2777  df-cleq 2791  df-clel 2870  df-nfc 2938  df-rab 3115  df-v 3443  df-un 3886  df-in 3888  df-ss 3898  df-sn 4526  df-pr 4528  df-op 4532  df-br 5031  df-opab 5093  df-xp 5525  df-cnv 5527  df-dm 5529  df-rn 5530  df-res 5531  df-ima 5532
This theorem is referenced by:  imaeq12d  5897  nfimad  5905  csbima12  5914  elimasng  5922  elimasni  5923  inisegn0  5928  csbrn  6027  ressn  6104  foima  6570  f1imacnv  6606  dffv3  6641  fvco2  6735  fimacnvinrn2  6818  fsn2  6875  funfvima3  6976  isofrlem  7072  isoselem  7073  fnexALT  7634  curry1  7782  curry2  7785  fparlem3  7792  fparlem4  7793  suppsnop  7827  ressuppssdif  7834  suppco  7853  imacosupp  7857  imacosuppOLD  7858  eceq1  8310  uniqs2  8342  ecinxp  8355  mapsnd  8433  sbthlem2  8612  sbth  8621  phplem4  8683  php3  8687  marypha1lem  8881  cantnfp1lem3  9127  tcrank  9297  fin4en1  9720  fin1a2lem7  9817  hsmexlem4  9840  hsmexlem5  9841  fpwwe2cbv  10041  fpwwe2lem3  10044  fpwwe2lem13  10053  fpwwecbv  10055  canth4  10058  frnnn0fsupp  11942  resunimafz0  13799  limsupgval  14825  isercoll  15016  vdwlem1  16307  vdwlem6  16312  vdwlem7  16313  vdwlem8  16314  vdwlem12  16318  vdwlem13  16319  vdwnn  16324  0ram  16346  ramz2  16350  isacs1i  16920  acsficl  17773  gsumvalx  17878  gsumpropd  17880  gsumpropd2lem  17881  gsumress  17884  efgrelexlema  18867  gsumval3a  19016  gsumval3lem1  19018  gsum2dlem2  19084  gsum2d2  19087  dprddisj  19124  dprdf1o  19147  dprdsn  19151  dprd2dlem2  19155  dprd2dlem1  19156  dprd2da  19157  dprd2db  19158  dmdprdsplit2lem  19160  dpjfval  19170  frlmup3  20489  islindf  20501  islindf2  20503  lindfind  20505  f1lindf  20511  lmimlbs  20525  coe1mul2lem2  20897  subbascn  21859  cncls2  21878  cncls  21879  cnntr  21880  cnpresti  21893  cnprest  21894  cnt1  21955  cnhaus  21959  cncmp  21997  cnconn  22027  1stcfb  22050  xkoccn  22224  ptrescn  22244  xkococnlem  22264  qtopeu  22321  qtoprest  22322  kqdisj  22337  kqcldsat  22338  ordthmeolem  22406  fmfnfmlem4  22562  ustuqtoplem  22845  utopsnneiplem  22853  utopsnneip  22854  ucncn  22891  metustto  23160  metustexhalf  23163  metustfbas  23164  cfilucfil  23166  metuust  23167  cfilucfil2  23168  metuel  23171  metuel2  23172  psmetutop  23174  restmetu  23177  metucn  23178  pi1addval  23653  iscph  23775  cphsscph  23855  uniioombllem3  24189  dyadmbl  24204  mbfima  24234  mbfimaicc  24235  mbfimasn  24236  ismbfd  24243  ismbf2d  24244  ismbf3d  24258  mbfimaopnlem  24259  i1fd  24285  i1f1  24294  itg11  24295  i1faddlem  24297  i1fmullem  24298  i1fadd  24299  itg1addlem3  24302  itg1mulc  24308  itg2gt0  24364  limcnlp  24481  ellimc3  24482  limcflf  24484  limciun  24497  mdegval  24664  mdeg0  24671  mdegvsca  24677  mdegpropd  24685  deg1val  24697  ig1pval  24773  coeeu  24822  coeeq  24824  pserulm  25017  areambl  25544  pthdlem2  27557  eupth2lem3  28021  eupth2  28024  issh  28991  isch  29005  shsval  29095  sspreima  30406  2ndimaxp  30409  fnpreimac  30434  dfcnv2  30439  s2rn  30646  s3rn  30648  swrdrndisj  30657  pwrssmgc  30706  gsummpt2co  30733  gsumpart  30740  gsumhashmul  30741  cycpmco2rn  30817  elrspunidl  31014  rhmimaidl  31017  dimval  31089  dimvalfi  31090  extdgval  31132  smatrcl  31149  locfinreflem  31193  zarclsint  31225  rhmpreimacn  31238  zrhunitpreima  31329  mbfmco2  31633  sibfima  31706  sibfof  31708  eulerpartlemgv  31741  eulerpartlemn  31749  eulerpart  31750  orvcval4  31828  orvcelval  31836  orvcelel  31837  ballotlemscr  31886  f1resfz0f1d  32471  pthhashvtx  32484  erdszelem3  32550  erdsze  32559  cvmliftlem3  32644  cvmliftlem7  32648  cvmlift2lem9a  32660  msrval  32895  mvtinf  32912  mclsval  32920  mclsax  32926  mthmpps  32939  opelco3  33128  scutval  33375  madeval  33399  funpartlem  33513  tailval  33831  csbpredg  34740  ptrest  35053  poimirlem1  35055  poimirlem2  35056  poimirlem3  35057  poimirlem4  35058  poimirlem5  35059  poimirlem6  35060  poimirlem7  35061  poimirlem9  35063  poimirlem10  35064  poimirlem11  35065  poimirlem12  35066  poimirlem13  35067  poimirlem14  35068  poimirlem15  35069  poimirlem16  35070  poimirlem17  35071  poimirlem19  35073  poimirlem20  35074  poimirlem22  35076  poimirlem23  35077  poimirlem24  35078  poimirlem25  35079  poimirlem26  35080  poimirlem27  35081  poimirlem28  35082  poimirlem29  35083  poimirlem31  35085  poimirlem32  35086  mblfinlem2  35092  volsupnfl  35099  itg2addnclem2  35106  sstotbnd2  35209  ismtyhmeolem  35239  grpokerinj  35328  lkrfval  36380  dnnumch3lem  39985  aomclem8  40000  pwfi2f1o  40035  cytpval  40148  frege97d  40448  frege109d  40453  frege131d  40460  nzprmdif  41018  wessf1ornlem  41806  limsuplesup  42336  limsupvaluz  42345  limsuplt2  42390  limsupge  42398  liminfgval  42399  liminfval2  42405  liminflelimsuplem  42412  liminflelimsup  42413  preimaioomnf  43349  afv2co2  43808  imarnf1pr  43833  preimafvelsetpreimafv  43900  imaelsetpreimafv  43907  imasetpreimafvbijlemfo  43917  fundcmpsurbijinjpreimafv  43919  fundcmpsurinj  43921  fundcmpsurbijinj  43922  isomgr  44336  isomushgr  44339  isomgrsym  44349  isomgrtrlem  44351
  Copyright terms: Public domain W3C validator