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

Theorem coeq12d 4956
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 4953 . 2  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  C ) )
3 coeq12d.2 . . 3  |-  ( ph  ->  C  =  D )
43coeq2d 4954 . 2  |-  ( ph  ->  ( B  o.  C
)  =  ( B  o.  D ) )
52, 4eqtrd 2457 1  |-  ( ph  ->  ( A  o.  C
)  =  ( B  o.  D ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    = wceq 1437    o. ccom 4795
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2058  ax-ext 2403
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2410  df-cleq 2416  df-clel 2419  df-nfc 2553  df-in 3381  df-ss 3388  df-br 4362  df-opab 4421  df-co 4800
This theorem is referenced by:  xpcoid  5334  dfac12lem1  8519  dfac12r  8522  trcleq2lem  12994  trclfvcotrg  13019  relexpaddg  13055  dfrtrcl2  13064  imasval  15349  imasvalOLD  15350  cofuval  15725  cofu2nd  15728  cofuval2  15730  cofuass  15732  cofurid  15734  setcco  15916  estrcco  15953  funcestrcsetclem9  15971  funcsetcestrclem9  15986  isdir  16416  evl1fval  18854  znval  19043  znle2  19061  mdetfval  19548  mdetdiaglem  19560  ust0  21171  trust  21181  metustexhalf  21508  isngp  21547  ngppropd  21582  tngval  21584  tngngp2  21597  imsval  26254  opsqrlem3  27732  hmopidmch  27743  hmopidmpj  27744  pjidmco  27771  dfpjop  27772  zhmnrg  28718  istendo  34239  tendoco2  34247  tendoidcl  34248  tendococl  34251  tendoplcbv  34254  tendopl2  34256  tendoplco2  34258  tendodi1  34263  tendodi2  34264  tendo0co2  34267  tendoicl  34275  erngplus2  34283  erngplus2-rN  34291  cdlemk55u1  34444  cdlemk55u  34445  dvaplusgv  34489  dvhopvadd  34573  dvhlveclem  34588  dvhopaddN  34594  dicvaddcl  34670  dihopelvalcpre  34728  rtrclex  36137  trclubgNEW  36138  rtrclexi  36141  cnvtrcl0  36146  dfrtrcl5  36149  trcleq2lemRP  36150  csbcog  36154  trrelind  36170  trrelsuperreldg  36173  trficl  36174  trrelsuperrel2dg  36176  trclrelexplem  36216  relexpaddss  36223  dfrtrcl3  36238  rngccoALTV  39581  funcrngcsetcALT  39592  funcringcsetcALTV2lem9  39637  ringccoALTV  39644  funcringcsetclem9ALTV  39660
  Copyright terms: Public domain W3C validator