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

Theorem coeq2d 5317
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 5313 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1523  ccom 5147
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1762  ax-4 1777  ax-5 1879  ax-6 1945  ax-7 1981  ax-9 2039  ax-10 2059  ax-11 2074  ax-12 2087  ax-13 2282  ax-ext 2631
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1526  df-ex 1745  df-nf 1750  df-sb 1938  df-clab 2638  df-cleq 2644  df-clel 2647  df-nfc 2782  df-in 3614  df-ss 3621  df-br 4686  df-opab 4746  df-co 5152
This theorem is referenced by:  coeq12d  5319  f1ococnv1  6203  funcoeqres  6205  fcof1oinvd  6588  foeqcnvco  6595  fparlem3  7324  fparlem4  7325  mapen  8165  mapfien  8354  wemapwe  8632  hashfacen  13276  s1co  13625  relexpsucnnl  13816  relexpsucl  13817  relexpcnv  13819  relexpaddnn  13835  relexpaddg  13837  prdsval  16162  isofval  16464  cofuass  16596  cofurid  16598  fucid  16678  setcinv  16787  catcisolem  16803  curf2ndf  16934  pwsco2mhm  17418  symggrp  17866  f1omvdco2  17914  psgnunilem1  17959  efginvrel2  18186  efginvrel1  18187  vrgpinv  18228  frgpuplem  18231  gsumval3  18354  gsumzf1o  18359  psrass1lem  19425  mpfrcl  19566  evlsval  19567  evls1fval  19732  evl1fval  19740  pf1mpf  19764  pf1ind  19767  ofco2  20305  qtophmeo  21668  ustssco  22065  utop2nei  22101  neipcfilu  22147  tngds  22499  elovolmr  23290  ovoliunlem3  23318  uniioombllem2  23397  hoddi  28977  fcoinver  29544  fmptco1f1o  29562  fcobij  29628  symgfcoeu  29973  smatfval  29989  eulerpartlemgv  30563  eulerpartlemn  30571  eulerpart  30572  sseqval  30578  reprpmtf1o  30832  erdsze2lem2  31312  cvmliftlem10  31402  mrsubval  31532  dfpo2  31771  ftc1anclem8  33622  cocnv  33650  ltrncoidN  35732  trlcoabs2N  36327  cdlemg47a  36339  cdlemg46  36340  cdlemg47  36341  ltrnco4  36344  tendovalco  36370  tendoplcbv  36380  tendopl  36381  tendoplass  36388  cdlemi2  36424  cdlemk2  36437  cdlemk4  36439  cdlemk8  36443  cdlemkuu  36500  cdlemk53  36562  cdlemk54  36563  cdlemk55a  36564  erngdvlem3  36595  erngdvlem3-rN  36603  tendocnv  36627  tendospcanN  36629  dvhvaddcbv  36695  dvhvaddval  36696  dvhvaddass  36703  dvhvscacbv  36704  dvhvscaval  36705  dvhopvsca  36708  dvhlveclem  36714  dvhopspN  36721  diblss  36776  cdlemn8  36810  dihopelvalcpre  36854  dihmeetlem1N  36896  dihglblem5apreN  36897  dih1dimatlem0  36934  dihjatcclem4  37027  diophrw  37639  eldioph2  37642  relexpaddss  38327  trclfvcom  38332  frege131d  38373  fsovrfovd  38620  hoicvrrex  41091  ovnlecvr  41093  ovncvrrp  41099  ovn0lem  41100  ovnsubaddlem1  41105  ovnsubadd  41107  ovnhoilem1  41136  ovnhoi  41138  ovnlecvr2  41145  ovncvr2  41146  hspmbl  41164  ovnovollem1  41191  ovnovollem3  41193  pfxco  41763
  Copyright terms: Public domain W3C validator