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

Theorem coeq2d 5823
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 5819 . 2 (𝐴 = 𝐵 → (𝐶𝐴) = (𝐶𝐵))
31, 2syl 17 1 (𝜑 → (𝐶𝐴) = (𝐶𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ccom 5642
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-br 5111  df-opab 5173  df-co 5647
This theorem is referenced by:  coeq12d  5825  dfpo2  6253  f1ococnv1  6818  funcoeqres  6820  fcof1oinvd  7244  foeqcnvco  7251  f1ofvswap  7257  fparlem3  8051  fparlem4  8052  offsplitfpar  8056  csbwrecsg  8257  mapen  9092  mapfien  9351  wemapwe  9640  hashfacen  14358  hashfacenOLD  14359  s1co  14729  pfxco  14734  relexpsucnnl  14922  relexpsucl  14923  relexpsucld  14926  relexpcnv  14927  relexpaddnn  14943  relexpaddg  14945  prdsval  17344  isofval  17647  cofuass  17782  cofurid  17784  fucid  17867  setcinv  17983  catcisolem  18003  curf2ndf  18143  pwsco2mhm  18650  symggrplem  18701  smndex1igid  18721  f1omvdco2  19237  psgnunilem1  19282  efginvrel2  19516  efginvrel1  19517  vrgpinv  19558  frgpuplem  19561  gsumval3  19691  gsumzf1o  19696  psrass1lemOLD  21358  psrass1lem  21361  mpfrcl  21511  evlsval  21512  selvval  21544  evls1fval  21701  evl1fval  21710  pf1mpf  21734  pf1ind  21737  ofco2  21816  qtophmeo  23184  ustssco  23582  utop2nei  23618  neipcfilu  23664  tngds  24027  tngdsOLD  24028  elovolmr  24856  ovoliunlem3  24884  uniioombllem2  24963  hoddi  30974  fcoinver  31567  fmptco1f1o  31589  fcobij  31681  symgfcoeu  31975  symgcom  31976  tocycf  32008  tocyc01  32009  cycpmconjvlem  32032  cycpmconjv  32033  cycpmconjslem1  32045  cycpmconjslem2  32046  cycpmconjs  32047  cyc3conja  32048  smatfval  32416  eulerpartlemgv  33013  eulerpartlemn  33021  eulerpart  33022  sseqval  33028  reprpmtf1o  33279  erdsze2lem2  33838  cvmliftlem10  33928  mrsubval  34143  ftc1anclem8  36187  cocnv  36213  ltrncoidN  38620  trlcoabs2N  39214  cdlemg47a  39226  cdlemg46  39227  cdlemg47  39228  ltrnco4  39231  tendovalco  39257  tendoplcbv  39267  tendopl  39268  tendoplass  39275  cdlemi2  39311  cdlemk2  39324  cdlemk4  39326  cdlemk8  39330  cdlemkuu  39387  cdlemk53  39449  cdlemk54  39450  cdlemk55a  39451  erngdvlem3  39482  erngdvlem3-rN  39490  tendocnv  39513  tendospcanN  39515  dvhvaddcbv  39581  dvhvaddval  39582  dvhvaddass  39589  dvhvscacbv  39590  dvhvscaval  39591  dvhopvsca  39594  dvhlveclem  39600  dvhopspN  39607  diblss  39662  cdlemn8  39696  dihopelvalcpre  39740  dihmeetlem1N  39782  dihglblem5apreN  39783  dih1dimatlem0  39820  dihjatcclem4  39913  mhmcoaddmpl  40768  rhmcomulmpl  40769  rhmmpl  40770  diophrw  41111  eldioph2  41114  relexpaddss  42064  trclfvcom  42069  frege131d  42110  fsovrfovd  42355  hoicvrrex  44871  ovnlecvr  44873  ovncvrrp  44879  ovn0lem  44880  ovnsubaddlem1  44885  ovnsubadd  44887  ovnhoilem1  44916  ovnhoi  44918  ovnlecvr2  44925  ovncvr2  44926  hspmbl  44944  ovnovollem1  44971  ovnovollem3  44973
  Copyright terms: Public domain W3C validator