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

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

Proof of Theorem coeq1d
StepHypRef Expression
1 coeq1d.1 . 2 (𝜑𝐴 = 𝐵)
2 coeq1 5814 . 2 (𝐴 = 𝐵 → (𝐴𝐶) = (𝐵𝐶))
31, 2syl 17 1 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ccom 5638
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 2704
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3446  df-in 3918  df-ss 3928  df-br 5107  df-opab 5169  df-co 5643
This theorem is referenced by:  coeq12d  5821  fcof1oinvd  7240  domss2  9083  mapen  9088  mapfien  9349  hashfacen  14357  hashfacenOLD  14358  relexpsucnnr  14916  relexpsucnnl  14921  relexpsucr  14923  relexpsucrd  14924  relexpaddnn  14942  imasval  17398  cofuass  17780  cofulid  17781  setcinv  17981  catcisolem  18001  catciso  18002  yonedalem3b  18173  gsumvalx  18536  frmdup3lem  18681  symggrplem  18699  f1omvdco2  19235  symggen  19257  psgnunilem1  19280  gsumval3  19689  gsumzf1o  19694  znval  20954  znle2  20976  psrass1lemOLD  21358  psrass1lem  21361  coe1add  21651  evls1fval  21701  evl1sca  21716  evl1var  21718  evls1var  21720  pf1mpf  21734  pf1ind  21737  tcphds  24611  dvnfval  25302  hocsubdir  30769  fcoinver  31571  fcobij  31686  symgfcoeu  31982  symgcom  31983  pmtrcnel2  31990  tocyc01  32016  cycpm2tr  32017  cycpmconjv  32040  cycpmconjslem1  32052  cycpmconjslem2  32053  cycpmconjs  32054  cyc3conja  32055  reprpmtf1o  33296  hgt750lemg  33324  subfacp1lem5  33835  mrsubffval  34158  mrsubfval  34159  mrsubrn  34164  elmrsubrn  34171  upixp  36234  ltrncoidN  38637  trlcoat  39232  trlcone  39237  cdlemg47a  39243  cdlemg47  39245  ltrnco4  39248  tendovalco  39274  tendoplcbv  39284  tendopl  39285  tendoplass  39292  tendo0pl  39300  tendoipl  39306  cdlemk45  39456  cdlemk53b  39465  cdlemk55a  39468  erngdvlem3  39499  erngdvlem3-rN  39507  tendocnv  39530  dvhvaddcbv  39598  dvhvaddval  39599  dvhvaddass  39606  dicvscacl  39700  cdlemn8  39713  dihordlem7b  39724  dihopelvalcpre  39757  relexp2  42037  relexpxpnnidm  42063  relexpiidm  42064  relexpmulnn  42069  relexpaddss  42078  trclfvcom  42083  trclfvdecomr  42088  frege131d  42124  dssmap2d  42382  fundcmpsurbijinjpreimafv  45685  isomushgr  46104
  Copyright terms: Public domain W3C validator