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

Theorem coeq12d 5817
Description: Equality deduction for composition of two classes. (Contributed by FL, 7-Jun-2012.)
Hypotheses
Ref Expression
coeq12d.1 (𝜑𝐴 = 𝐵)
coeq12d.2 (𝜑𝐶 = 𝐷)
Assertion
Ref Expression
coeq12d (𝜑 → (𝐴𝐶) = (𝐵𝐷))

Proof of Theorem coeq12d
StepHypRef Expression
1 coeq12d.1 . . 3 (𝜑𝐴 = 𝐵)
21coeq1d 5814 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 coeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43coeq2d 5815 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2778 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1542  ccom 5635
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2709
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-in 3916  df-ss 3926  df-br 5105  df-opab 5167  df-co 5640
This theorem is referenced by:  relcnvtrg  6215  xpcoid  6239  csbcog  6246  dfac12lem1  10013  dfac12r  10016  trcleq2lem  14811  trclfvcotrg  14836  relexpaddg  14873  relexpaddd  14874  dfrtrcl2  14882  imasval  17329  cofuval  17704  cofu2nd  17707  cofuval2  17709  cofuass  17711  cofurid  17713  setcco  17905  estrcco  17953  funcestrcsetclem9  17972  funcsetcestrclem9  17987  isdir  18423  smndex1mgm  18653  symgov  19100  znval  20867  znle2  20889  evl1fval  21622  mdetfval  21863  mdetdiaglem  21875  ust0  23499  trust  23509  metustexhalf  23840  isngp  23880  ngppropd  23921  tngval  23923  tngngp2  23944  imsval  29432  opsqrlem3  30889  hmopidmch  30900  hmopidmpj  30901  pjidmco  30928  dfpjop  30929  cosnop  31411  tocycfv  31759  cycpm2tr  31769  cyc3genpmlem  31801  cycpmconjslem2  31805  cycpmconjs  31806  cyc3conja  31807  zhmnrg  32328  bj-imdirco  35592  dftrrels2  36968  dftrrel2  36970  istendo  39154  tendoco2  39162  tendoidcl  39163  tendococl  39166  tendoplcbv  39169  tendopl2  39171  tendoplco2  39173  tendodi1  39178  tendodi2  39179  tendo0co2  39182  tendoicl  39190  erngplus2  39198  erngplus2-rN  39206  cdlemk55u1  39359  cdlemk55u  39360  dvaplusgv  39404  dvhopvadd  39487  dvhlveclem  39502  dvhopaddN  39508  dicvaddcl  39584  dihopelvalcpre  39642  rtrclex  41688  trclubgNEW  41689  rtrclexi  41692  cnvtrcl0  41697  dfrtrcl5  41700  trcleq2lemRP  41701  trrelind  41736  trrelsuperreldg  41739  trficl  41740  trrelsuperrel2dg  41742  trclrelexplem  41782  relexpaddss  41789  dfrtrcl3  41804  clsneicnv  42178  neicvgnvo  42188  fundcmpsurbijinjpreimafv  45390  fundcmpsurinjALT  45395  rngccoALTV  46077  funcrngcsetcALT  46088  funcringcsetcALTV2lem9  46133  ringccoALTV  46140  funcringcsetclem9ALTV  46156
  Copyright terms: Public domain W3C validator