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

Theorem coeq12d 5196
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 5193 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 coeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43coeq2d 5194 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2643 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1474  ccom 5032
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-in 3546  df-ss 3553  df-br 4578  df-opab 4638  df-co 5037
This theorem is referenced by:  xpcoid  5579  dfac12lem1  8825  dfac12r  8828  trcleq2lem  13524  trclfvcotrg  13551  relexpaddg  13587  dfrtrcl2  13596  imasval  15940  cofuval  16311  cofu2nd  16314  cofuval2  16316  cofuass  16318  cofurid  16320  setcco  16502  estrcco  16539  funcestrcsetclem9  16557  funcsetcestrclem9  16572  isdir  17001  evl1fval  19459  znval  19647  znle2  19666  mdetfval  20153  mdetdiaglem  20165  ust0  21775  trust  21785  metustexhalf  22112  isngp  22151  ngppropd  22189  tngval  22191  tngngp2  22204  imsval  26721  opsqrlem3  28191  hmopidmch  28202  hmopidmpj  28203  pjidmco  28230  dfpjop  28231  zhmnrg  29145  istendo  34862  tendoco2  34870  tendoidcl  34871  tendococl  34874  tendoplcbv  34877  tendopl2  34879  tendoplco2  34881  tendodi1  34886  tendodi2  34887  tendo0co2  34890  tendoicl  34898  erngplus2  34906  erngplus2-rN  34914  cdlemk55u1  35067  cdlemk55u  35068  dvaplusgv  35112  dvhopvadd  35196  dvhlveclem  35211  dvhopaddN  35217  dicvaddcl  35293  dihopelvalcpre  35351  rtrclex  36739  trclubgNEW  36740  rtrclexi  36743  cnvtrcl0  36748  dfrtrcl5  36751  trcleq2lemRP  36752  csbcog  36756  trrelind  36772  trrelsuperreldg  36775  trficl  36776  trrelsuperrel2dg  36778  trclrelexplem  36818  relexpaddss  36825  dfrtrcl3  36840  clsneicnv  37219  neicvgnvo  37229  rngccoALTV  41775  funcrngcsetcALT  41786  funcringcsetcALTV2lem9  41831  ringccoALTV  41838  funcringcsetclem9ALTV  41854
  Copyright terms: Public domain W3C validator