MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  coeq12d Structured version   Unicode version

Theorem coeq12d 5019
Description: Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
Hypotheses
Ref Expression
coeq12d.1  |-  ( ph  ->  A  =  B )
coeq12d.2  |-  ( ph  ->  C  =  D )
Assertion
Ref Expression
coeq12d  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )

Proof of Theorem coeq12d
StepHypRef Expression
1 coeq12d.1 . . 3  |-  ( ph  ->  A  =  B )
21coeq1d 5016 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 5017 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2470 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    o. ccom 4858
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-in 3449  df-ss 3456  df-br 4427  df-opab 4485  df-co 4863
This theorem is referenced by:  xpcoid  5397  dfac12lem1  8571  dfac12r  8574  trcleq2lem  13034  trclfvcotrg  13059  relexpaddg  13095  dfrtrcl2  13104  imasval  15368  cofuval  15738  cofu2nd  15741  cofuval2  15743  cofuass  15745  cofurid  15747  setcco  15929  estrcco  15966  funcestrcsetclem9  15984  funcsetcestrclem9  15999  isdir  16429  evl1fval  18851  znval  19037  znle2  19055  mdetfval  19542  mdetdiaglem  19554  ust0  21165  trust  21175  metustexhalf  21502  isngp  21541  ngppropd  21576  tngval  21578  tngngp2  21591  imsval  26162  opsqrlem3  27630  hmopidmch  27641  hmopidmpj  27642  pjidmco  27669  dfpjop  27670  zhmnrg  28610  istendo  34036  tendoco2  34044  tendoidcl  34045  tendococl  34048  tendoplcbv  34051  tendopl2  34053  tendoplco2  34055  tendodi1  34060  tendodi2  34061  tendo0co2  34064  tendoicl  34072  erngplus2  34080  erngplus2-rN  34088  cdlemk55u1  34241  cdlemk55u  34242  dvaplusgv  34286  dvhopvadd  34370  dvhlveclem  34385  dvhopaddN  34391  dicvaddcl  34467  dihopelvalcpre  34525  csbcog  35880  trrelind  35896  trrelsuperreldg  35899  trficl  35900  trrelsuperrel2dg  35902  trclrelexplem  35942  relexpaddss  35949  dfrtrcl3  35964  rngccoALTV  38748  funcrngcsetcALT  38759  funcringcsetcALTV2lem9  38804  ringccoALTV  38811  funcringcsetclem9ALTV  38827
  Copyright terms: Public domain W3C validator