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

Theorem coeq12d 5023
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 5020 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 5021 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2462 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    o. ccom 4868
This theorem is referenced by:  xpcoid  5401  dfac12lem1  8007  dfac12r  8010  imasval  13720  cofuval  14062  cofu2nd  14065  cofuval2  14067  cofuass  14069  cofurid  14071  setcco  14221  isdir  14660  znval  16799  znle2  16817  ust0  18232  trust  18242  metustexhalfOLD  18576  metustexhalf  18577  isngp  18626  ngppropd  18661  tngval  18663  tngngp2  18676  evl1fval  19930  imsval  22160  opsqrlem3  23628  hmopidmch  23639  hmopidmpj  23640  pjidmco  23667  dfpjop  23668  zhmnrg  24334  dfrtrcl2  25131  istendo  31288  tendoco2  31296  tendoidcl  31297  tendococl  31300  tendoplcbv  31303  tendopl2  31305  tendoplco2  31307  tendodi1  31312  tendodi2  31313  tendo0co2  31316  tendoicl  31324  erngplus2  31332  erngplus2-rN  31340  cdlemk55u1  31493  cdlemk55u  31494  dvaplusgv  31538  dvhopvadd  31622  dvhlveclem  31637  dvhopaddN  31643  dicvaddcl  31719  dihopelvalcpre  31777
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-in 3314  df-ss 3321  df-br 4200  df-opab 4254  df-co 4873
  Copyright terms: Public domain W3C validator