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

Theorem coeq12d 5028
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 5025 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 5026 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2467 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff set class
Syntax hints:    -> wi 4    = wceq 1652    o. ccom 4873
This theorem is referenced by:  xpcoid  5406  dfac12lem1  8012  dfac12r  8015  imasval  13725  cofuval  14067  cofu2nd  14070  cofuval2  14072  cofuass  14074  cofurid  14076  setcco  14226  isdir  14665  znval  16804  znle2  16822  ust0  18237  trust  18247  metustexhalfOLD  18581  metustexhalf  18582  isngp  18631  ngppropd  18666  tngval  18668  tngngp2  18681  evl1fval  19935  imsval  22165  opsqrlem3  23633  hmopidmch  23644  hmopidmpj  23645  pjidmco  23672  dfpjop  23673  zhmnrg  24339  dfrtrcl2  25136  istendo  31396  tendoco2  31404  tendoidcl  31405  tendococl  31408  tendoplcbv  31411  tendopl2  31413  tendoplco2  31415  tendodi1  31420  tendodi2  31421  tendo0co2  31424  tendoicl  31432  erngplus2  31440  erngplus2-rN  31448  cdlemk55u1  31601  cdlemk55u  31602  dvaplusgv  31646  dvhopvadd  31730  dvhlveclem  31745  dvhopaddN  31751  dicvaddcl  31827  dihopelvalcpre  31885
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 2416
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 2422  df-cleq 2428  df-clel 2431  df-nfc 2560  df-in 3319  df-ss 3326  df-br 4205  df-opab 4259  df-co 4878
  Copyright terms: Public domain W3C validator