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

Theorem coeq12d 5728
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 5725 . 2 (𝜑 → (𝐴𝐶) = (𝐵𝐶))
3 coeq12d.2 . . 3 (𝜑𝐶 = 𝐷)
43coeq2d 5726 . 2 (𝜑 → (𝐵𝐶) = (𝐵𝐷))
52, 4eqtrd 2854 1 (𝜑 → (𝐴𝐶) = (𝐵𝐷))
Colors of variables: wff setvar class
Syntax hints:  wi 4   = wceq 1530  ccom 5552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2791
This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-clab 2798  df-cleq 2812  df-clel 2891  df-nfc 2961  df-in 3941  df-ss 3950  df-br 5058  df-opab 5120  df-co 5557
This theorem is referenced by:  relcnvtrg  6112  xpcoid  6134  dfac12lem1  9561  dfac12r  9564  trcleq2lem  14343  trclfvcotrg  14368  relexpaddg  14404  dfrtrcl2  14413  imasval  16776  cofuval  17144  cofu2nd  17147  cofuval2  17149  cofuass  17151  cofurid  17153  setcco  17335  estrcco  17372  funcestrcsetclem9  17390  funcsetcestrclem9  17405  isdir  17834  smndex1mgm  18064  symgov  18504  evl1fval  20483  znval  20674  znle2  20692  mdetfval  21187  mdetdiaglem  21199  ust0  22820  trust  22830  metustexhalf  23158  isngp  23197  ngppropd  23238  tngval  23240  tngngp2  23253  imsval  28454  opsqrlem3  29911  hmopidmch  29922  hmopidmpj  29923  pjidmco  29950  dfpjop  29951  cosnop  30423  tocycfv  30744  cycpm2tr  30754  cyc3genpmlem  30786  cycpmconjslem2  30790  cycpmconjs  30791  cyc3conja  30792  zhmnrg  31196  dftrrels2  35793  dftrrel2  35795  istendo  37878  tendoco2  37886  tendoidcl  37887  tendococl  37890  tendoplcbv  37893  tendopl2  37895  tendoplco2  37897  tendodi1  37902  tendodi2  37903  tendo0co2  37906  tendoicl  37914  erngplus2  37922  erngplus2-rN  37930  cdlemk55u1  38083  cdlemk55u  38084  dvaplusgv  38128  dvhopvadd  38211  dvhlveclem  38226  dvhopaddN  38232  dicvaddcl  38308  dihopelvalcpre  38366  rtrclex  39957  trclubgNEW  39958  rtrclexi  39961  cnvtrcl0  39966  dfrtrcl5  39969  trcleq2lemRP  39970  csbcog  39974  trrelind  39990  trrelsuperreldg  39993  trficl  39994  trrelsuperrel2dg  39996  trclrelexplem  40036  relexpaddss  40043  dfrtrcl3  40058  clsneicnv  40435  neicvgnvo  40445  fundcmpsurbijinjpreimafv  43547  fundcmpsurinjALT  43552  rngccoALTV  44239  funcrngcsetcALT  44250  funcringcsetcALTV2lem9  44295  ringccoALTV  44302  funcringcsetclem9ALTV  44318
  Copyright terms: Public domain W3C validator