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

Theorem coeq12d 4864
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 4861 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 4862 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2328 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1632    o. ccom 4709
This theorem is referenced by:  dfac12lem1  7785  dfac12r  7788  imasval  13430  cofuval  13772  cofu2nd  13775  cofuval2  13777  cofuass  13779  cofurid  13781  setcco  13931  isdir  14370  znval  16505  znle2  16523  isngp  18134  ngppropd  18169  tngval  18171  tngngp2  18184  evl1fval  19426  imsval  21270  opsqrlem3  22738  hmopidmch  22749  hmopidmpj  22750  pjidmco  22777  dfpjop  22778  dfrtrcl2  24060  cmp2morp  26061  cmp2morpcatt  26065  istendo  31571  tendoco2  31579  tendoidcl  31580  tendococl  31583  tendoplcbv  31586  tendopl2  31588  tendoplco2  31590  tendodi1  31595  tendodi2  31596  tendo0co2  31599  tendoicl  31607  erngplus2  31615  erngplus2-rN  31623  cdlemk55u1  31776  cdlemk55u  31777  dvaplusgv  31821  dvhopvadd  31905  dvhlveclem  31920  dvhopaddN  31926  dicvaddcl  32002  dihopelvalcpre  32060
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-in 3172  df-ss 3179  df-br 4040  df-opab 4094  df-co 4714
  Copyright terms: Public domain W3C validator