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

Theorem coeq12d 4848
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 4845 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 4846 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2315 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1623    o. ccom 4693
This theorem is referenced by:  dfac12lem1  7769  dfac12r  7772  imasval  13414  cofuval  13756  cofu2nd  13759  cofuval2  13761  cofuass  13763  cofurid  13765  setcco  13915  isdir  14354  znval  16489  znle2  16507  isngp  18118  ngppropd  18153  tngval  18155  tngngp2  18168  evl1fval  19410  imsval  21254  opsqrlem3  22722  hmopidmch  22733  hmopidmpj  22734  pjidmco  22761  dfpjop  22762  dfrtrcl2  24045  cmp2morp  25958  cmp2morpcatt  25962  istendo  30949  tendoco2  30957  tendoidcl  30958  tendococl  30961  tendoplcbv  30964  tendopl2  30966  tendoplco2  30968  tendodi1  30973  tendodi2  30974  tendo0co2  30977  tendoicl  30985  erngplus2  30993  erngplus2-rN  31001  cdlemk55u1  31154  cdlemk55u  31155  dvaplusgv  31199  dvhopvadd  31283  dvhlveclem  31298  dvhopaddN  31304  dicvaddcl  31380  dihopelvalcpre  31438
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-in 3159  df-ss 3166  df-br 4024  df-opab 4078  df-co 4698
  Copyright terms: Public domain W3C validator