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  14810  trclfvcotrg  14835  relexpaddg  14872  relexpaddd  14873  dfrtrcl2  14881  imasval  17328  cofuval  17703  cofu2nd  17706  cofuval2  17708  cofuass  17710  cofurid  17712  setcco  17904  estrcco  17952  funcestrcsetclem9  17971  funcsetcestrclem9  17986  isdir  18422  smndex1mgm  18652  symgov  19098  znval  20862  znle2  20884  evl1fval  21617  mdetfval  21858  mdetdiaglem  21870  ust0  23494  trust  23504  metustexhalf  23835  isngp  23875  ngppropd  23916  tngval  23918  tngngp2  23939  imsval  29426  opsqrlem3  30883  hmopidmch  30894  hmopidmpj  30895  pjidmco  30922  dfpjop  30923  cosnop  31405  tocycfv  31753  cycpm2tr  31763  cyc3genpmlem  31795  cycpmconjslem2  31799  cycpmconjs  31800  cyc3conja  31801  zhmnrg  32322  bj-imdirco  35557  dftrrels2  36933  dftrrel2  36935  istendo  39119  tendoco2  39127  tendoidcl  39128  tendococl  39131  tendoplcbv  39134  tendopl2  39136  tendoplco2  39138  tendodi1  39143  tendodi2  39144  tendo0co2  39147  tendoicl  39155  erngplus2  39163  erngplus2-rN  39171  cdlemk55u1  39324  cdlemk55u  39325  dvaplusgv  39369  dvhopvadd  39452  dvhlveclem  39467  dvhopaddN  39473  dicvaddcl  39549  dihopelvalcpre  39607  rtrclex  41652  trclubgNEW  41653  rtrclexi  41656  cnvtrcl0  41661  dfrtrcl5  41664  trcleq2lemRP  41665  trrelind  41700  trrelsuperreldg  41703  trficl  41704  trrelsuperrel2dg  41706  trclrelexplem  41746  relexpaddss  41753  dfrtrcl3  41768  clsneicnv  42142  neicvgnvo  42152  fundcmpsurbijinjpreimafv  45354  fundcmpsurinjALT  45359  rngccoALTV  46041  funcrngcsetcALT  46052  funcringcsetcALTV2lem9  46097  ringccoALTV  46104  funcringcsetclem9ALTV  46120
  Copyright terms: Public domain W3C validator