Theorem coeq1 5165

Description: Equality theorem for composition of two classes. (Contributed by NM, 3-Jan-1997.)

Assertion

Ref	Expression
coeq1

Proof of Theorem coeq1

Step	Hyp	Ref	Expression
1		coss1 5163	. . 3
2		coss1 5163	. . 3
3	1, 2	anim12i 566	. 2
4		eqss 3518	. 2
5		eqss 3518	. 2
6	3, 4, 5	3imtr4i 266	1

Syntax hints:  ->wi 4  /\wa 369  =wceq 1395  C_wss 3475  o.ccom 5008

This theorem is referenced by:  coeq1i  5167  coeq1d  5169  coi2  5529  relcnvtr  5532  funcoeqres  5851  ereq1  7337  domssex2  7697  wemapwe  8160  wemapweOLD  8161  seqf1olem2  12147  seqf1o  12148  isps  15832  pwsco1mhm  16001  frmdup3  16035  symgov  16415  pmtr3ncom  16500  psgnunilem1  16518  frgpup3  16796  gsumval3OLD  16908  gsumval3  16911  evlseu  18185  evlsval2  18189  evls1val  18357  evls1sca  18360  evl1val  18365  mpfpf1  18387  pf1mpf  18388  pf1ind  18391  frgpcyg  18612  frlmup4  18835  xkococnlem  20160  xkococn  20161  cnmpt1k  20183  cnmptkk  20184  xkofvcn  20185  qtopeu  20217  qtophmeo  20318  utop2nei  20753  cncombf  22065  dgrcolem2  22671  dgrco  22672  motplusg  23929  hocsubdir  26704  hoddi  26909  opsqrlem1  27059  msubco  28891  relexpsucr  29053  relexp1  29054  relexpsucl  29055  diophrw  30692  eldioph2  30695  diophren  30747  mendmulr  31137  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  trljco  36466  tgrpov  36474  tendovalco  36491  erngmul  36532  erngmul-rN  36540  cdlemksv  36570  cdlemkuu  36621  cdlemk41  36646  cdleml5N  36706  cdleml9  36710  dvamulr  36738  dvavadd  36741  dvhmulr  36813  dvhvscacbv  36825  dvhvscaval  36826  dih1dimatlem0  37055  dihjatcclem4  37148

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