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

Theorem coeq12d 5040
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 5037 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 5038 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2470 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1653    o. ccom 4885
This theorem is referenced by:  xpcoid  5418  dfac12lem1  8028  dfac12r  8031  imasval  13742  cofuval  14084  cofu2nd  14087  cofuval2  14089  cofuass  14091  cofurid  14093  setcco  14243  isdir  14682  znval  16821  znle2  16839  ust0  18254  trust  18264  metustexhalfOLD  18598  metustexhalf  18599  isngp  18648  ngppropd  18683  tngval  18685  tngngp2  18698  evl1fval  19952  imsval  22182  opsqrlem3  23650  hmopidmch  23661  hmopidmpj  23662  pjidmco  23689  dfpjop  23690  zhmnrg  24356  dfrtrcl2  25153  istendo  31631  tendoco2  31639  tendoidcl  31640  tendococl  31643  tendoplcbv  31646  tendopl2  31648  tendoplco2  31650  tendodi1  31655  tendodi2  31656  tendo0co2  31659  tendoicl  31667  erngplus2  31675  erngplus2-rN  31683  cdlemk55u1  31836  cdlemk55u  31837  dvaplusgv  31881  dvhopvadd  31965  dvhlveclem  31980  dvhopaddN  31986  dicvaddcl  32062  dihopelvalcpre  32120
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-in 3329  df-ss 3336  df-br 4216  df-opab 4270  df-co 4890
  Copyright terms: Public domain W3C validator