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

Theorem coeq2d 5486
Description: Equality deduction for composition of two classes. (Contributed by NM, 16-Nov-2000.)
Hypothesis
Ref Expression
coeq1d.1 (𝜑𝐴 = 𝐵)
Assertion
Ref Expression
coeq2d (𝜑 → (𝐶𝐴) = (𝐶𝐵))

Proof of Theorem coeq2d
StepHypRef Expression
1 coeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 coeq2 5482 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1637  ccom 5315
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 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-in 3776  df-ss 3783  df-br 4845  df-opab 4907  df-co 5320
This theorem is referenced by:  coeq12d  5488  f1ococnv1  6381  funcoeqres  6383  fcof1oinvd  6772  foeqcnvco  6779  fparlem3  7513  fparlem4  7514  mapen  8363  mapfien  8552  wemapwe  8841  hashfacen  13455  s1co  13803  relexpsucnnl  13995  relexpsucl  13996  relexpcnv  13998  relexpaddnn  14014  relexpaddg  14016  prdsval  16320  isofval  16621  cofuass  16753  cofurid  16755  fucid  16835  setcinv  16944  catcisolem  16960  curf2ndf  17092  pwsco2mhm  17576  symggrp  18021  f1omvdco2  18069  psgnunilem1  18114  efginvrel2  18341  efginvrel1  18342  vrgpinv  18383  frgpuplem  18386  gsumval3  18509  gsumzf1o  18514  psrass1lem  19586  mpfrcl  19726  evlsval  19727  evls1fval  19892  evl1fval  19900  pf1mpf  19924  pf1ind  19927  ofco2  20468  qtophmeo  21834  ustssco  22231  utop2nei  22267  neipcfilu  22313  tngds  22665  elovolmr  23457  ovoliunlem3  23485  uniioombllem2  23564  hoddi  29177  fcoinver  29743  fmptco1f1o  29761  fcobij  29827  symgfcoeu  30170  smatfval  30186  eulerpartlemgv  30760  eulerpartlemn  30768  eulerpart  30769  sseqval  30775  reprpmtf1o  31029  erdsze2lem2  31509  cvmliftlem10  31599  mrsubval  31729  dfpo2  31967  ftc1anclem8  33804  cocnv  33832  ltrncoidN  35908  trlcoabs2N  36503  cdlemg47a  36515  cdlemg46  36516  cdlemg47  36517  ltrnco4  36520  tendovalco  36546  tendoplcbv  36556  tendopl  36557  tendoplass  36564  cdlemi2  36600  cdlemk2  36613  cdlemk4  36615  cdlemk8  36619  cdlemkuu  36676  cdlemk53  36738  cdlemk54  36739  cdlemk55a  36740  erngdvlem3  36771  erngdvlem3-rN  36779  tendocnv  36802  tendospcanN  36804  dvhvaddcbv  36870  dvhvaddval  36871  dvhvaddass  36878  dvhvscacbv  36879  dvhvscaval  36880  dvhopvsca  36883  dvhlveclem  36889  dvhopspN  36896  diblss  36951  cdlemn8  36985  dihopelvalcpre  37029  dihmeetlem1N  37071  dihglblem5apreN  37072  dih1dimatlem0  37109  dihjatcclem4  37202  diophrw  37824  eldioph2  37827  relexpaddss  38510  trclfvcom  38515  frege131d  38556  fsovrfovd  38803  hoicvrrex  41252  ovnlecvr  41254  ovncvrrp  41260  ovn0lem  41261  ovnsubaddlem1  41266  ovnsubadd  41268  ovnhoilem1  41297  ovnhoi  41299  ovnlecvr2  41306  ovncvr2  41307  hspmbl  41325  ovnovollem1  41352  ovnovollem3  41354  pfxco  42013
  Copyright terms: Public domain W3C validator