Theorem coeq12d 5172

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

Step	Hyp	Ref	Expression
1		coeq12d.1	. . 3
2	1	coeq1d 5169	. 2
3		coeq12d.2	. . 3
4	3	coeq2d 5170	. 2
5	2, 4	eqtrd 2498	1

Syntax hints:  ->wi 4  =wceq 1395  o.ccom 5008

This theorem is referenced by:  xpcoid  5553  dfac12lem1  8544  dfac12r  8547  imasval  14908  cofuval  15251  cofu2nd  15254  cofuval2  15256  cofuass  15258  cofurid  15260  setcco  15410  isdir  15862  evl1fval  18364  znval  18572  znle2  18592  mdetfval  19088  mdetdiaglem  19100  ust0  20722  trust  20732  metustexhalfOLD  21066  metustexhalf  21067  isngp  21116  ngppropd  21151  tngval  21153  tngngp2  21166  imsval  25591  opsqrlem3  27061  hmopidmch  27072  hmopidmpj  27073  pjidmco  27100  dfpjop  27101  zhmnrg  27948  dfrtrcl2  29071  estrcco  32636  funcestrcsetclem9  32654  funcsetcestrclem9  32669  rngccoOLD  32796  funcrngcsetcALT  32807  funcringcsetcOLD2lem9  32852  ringccoOLD  32859  funcringcsetclem9OLD  32875  istendo  36486  tendoco2  36494  tendoidcl  36495  tendococl  36498  tendoplcbv  36501  tendopl2  36503  tendoplco2  36505  tendodi1  36510  tendodi2  36511  tendo0co2  36514  tendoicl  36522  erngplus2  36530  erngplus2-rN  36538  cdlemk55u1  36691  cdlemk55u  36692  dvaplusgv  36736  dvhopvadd  36820  dvhlveclem  36835  dvhopaddN  36841  dicvaddcl  36917  dihopelvalcpre  36975  trrelind  37778  trficl  37779  trrelsuperreldg  37783  trclub  37784  trclubg  37785

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-in 3482  df-ss 3489  df-br 4453  df-opab 4511  df-co 5013