Theorem coeq2 5166

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

Assertion

Ref	Expression
coeq2

Proof of Theorem coeq2

Step	Hyp	Ref	Expression
1		coss2 5164	. . 3
2		coss2 5164	. . 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:  coeq2i  5168  coeq2d  5170  coi2  5529  relcnvtr  5532  relcoi1  5541  f1eqcocnv  6204  ereq1  7337  seqf1olem2  12147  seqf1o  12148  isps  15832  pwsco2mhm  16002  gsumwmhm  16013  frmdgsum  16030  frmdup1  16032  frmdup2  16033  symgov  16415  pmtr3ncom  16500  psgnunilem1  16518  frgpuplem  16790  frgpupf  16791  frgpupval  16792  gsumval3eu  16907  gsumval3OLD  16908  gsumval3lem2  16910  kgencn2  20058  upxp  20124  uptx  20126  txcn  20127  xkococnlem  20160  xkococn  20161  cnmptk1  20182  cnmptkk  20184  xkofvcn  20185  imasdsf1olem  20876  pi1cof  21559  pi1coval  21560  elovolmr  21887  ovoliunlem3  21915  ismbf1  22033  motplusg  23929  hocsubdir  26704  hoddi  26909  lnopco0i  26923  opsqrlem1  27059  pjsdi2i  27076  pjin2i  27112  pjclem1  27114  eulerpartgbij  28311  cvmliftmo  28729  cvmliftlem14  28742  cvmliftiota  28746  cvmlift2lem13  28760  cvmlift2  28761  cvmliftphtlem  28762  cvmlift3lem2  28765  cvmlift3lem6  28769  cvmlift3lem7  28770  cvmlift3lem9  28772  cvmlift3  28773  msubco  28891  relexp0  29052  relexpsucr  29053  relexpsucl  29055  relexpadd  29061  ftc1anclem8  30097  upixp  30220  mendmulr  31137  rngcinv  32789  rngcinvOLD  32801  ringcinv  32840  ringcinvOLD  32864  trlcoat  36449  trljco  36466  tgrpov  36474  tendovalco  36491  erngmul  36532  erngmul-rN  36540  dvamulr  36738  dvavadd  36741  dvhmulr  36813  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