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

Theorem coeq2d 5206
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 5202 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1475  ccom 5042
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-in 3547  df-ss 3554  df-br 4584  df-opab 4644  df-co 5047
This theorem is referenced by:  coeq12d  5208  f1ococnv1  6078  funcoeqres  6080  fcof1oinvd  6448  foeqcnvco  6455  fparlem3  7166  fparlem4  7167  mapen  8009  mapfien  8196  wemapwe  8477  hashfacen  13095  s1co  13430  relexpsucnnl  13620  relexpsucl  13621  relexpcnv  13623  relexpaddnn  13639  relexpaddg  13641  prdsval  15938  isofval  16240  cofuass  16372  cofurid  16374  fucid  16454  setcinv  16563  catcisolem  16579  curf2ndf  16710  pwsco2mhm  17194  symggrp  17643  f1omvdco2  17691  psgnunilem1  17736  efginvrel2  17963  efginvrel1  17964  vrgpinv  18005  frgpuplem  18008  gsumval3  18131  gsumzf1o  18136  psrass1lem  19198  mpfrcl  19339  evlsval  19340  evls1fval  19505  evl1fval  19513  pf1mpf  19537  pf1ind  19540  ofco2  20076  qtophmeo  21430  ustssco  21828  utop2nei  21864  neipcfilu  21910  tngds  22262  elovolmr  23051  ovoliunlem3  23079  uniioombllem2  23157  hoddi  28233  fcoinver  28798  fcobij  28888  symgfcoeu  29176  smatfval  29189  eulerpartlemgv  29762  eulerpartlemn  29770  eulerpart  29771  sseqval  29777  erdsze2lem2  30440  cvmliftlem10  30530  mrsubval  30660  dfpo2  30898  ftc1anclem8  32662  cocnv  32690  ltrncoidN  34432  trlcoabs2N  35028  cdlemg47a  35040  cdlemg46  35041  cdlemg47  35042  ltrnco4  35045  tendovalco  35071  tendoplcbv  35081  tendopl  35082  tendoplass  35089  cdlemi2  35125  cdlemk2  35138  cdlemk4  35140  cdlemk8  35144  cdlemkuu  35201  cdlemk53  35263  cdlemk54  35264  cdlemk55a  35265  erngdvlem3  35296  erngdvlem3-rN  35304  tendocnv  35328  tendospcanN  35330  dvhvaddcbv  35396  dvhvaddval  35397  dvhvaddass  35404  dvhvscacbv  35405  dvhvscaval  35406  dvhopvsca  35409  dvhlveclem  35415  dvhopspN  35422  diblss  35477  cdlemn8  35511  dihopelvalcpre  35555  dihmeetlem1N  35597  dihglblem5apreN  35598  dih1dimatlem0  35635  dihjatcclem4  35728  diophrw  36340  eldioph2  36343  relexpaddss  37029  trclfvcom  37034  frege131d  37075  fsovrfovd  37323  hoicvrrex  39446  ovnlecvr  39448  ovncvrrp  39454  ovn0lem  39455  ovnsubaddlem1  39460  ovnsubadd  39462  ovnhoilem1  39491  ovnhoi  39493  ovnlecvr2  39500  ovncvr2  39501  hspmbl  39519  ovnovollem1  39546  ovnovollem3  39548  pfxco  40301
  Copyright terms: Public domain W3C validator