Theorem coass 5531

Description: Associative law for class composition. Theorem 27 of [Suppes] p. 64. Also Exercise 21 of [Enderton] p. 53. Interestingly, this law holds for any classes whatsoever, not just functions or even relations. (Contributed by NM, 27-Jan-1997.)

Assertion

Ref	Expression
coass

Proof of Theorem coass

Dummy variables are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		relco 5510	. 2
2		relco 5510	. 2
3		excom 1849	. . . 4
4		anass 649	. . . . 5
5	4	2exbii 1668	. . . 4
6	3, 5	bitr4i 252	. . 3
7		vex 3112	. . . . . . 7
8		vex 3112	. . . . . . 7
9	7, 8	brco 5178	. . . . . 6
10	9	anbi2i 694	. . . . 5
11	10	exbii 1667	. . . 4
12		vex 3112	. . . . 5
13	12, 8	opelco 5179	. . . 4
14		exdistr 1776	. . . 4
15	11, 13, 14	3bitr4i 277	. . 3
16		vex 3112	. . . . . . 7
17	12, 16	brco 5178	. . . . . 6
18	17	anbi1i 695	. . . . 5
19	18	exbii 1667	. . . 4
20	12, 8	opelco 5179	. . . 4
21		19.41v 1771	. . . . 5
22	21	exbii 1667	. . . 4
23	19, 20, 22	3bitr4i 277	. . 3
24	6, 15, 23	3bitr4i 277	. 2
25	1, 2, 24	eqrelriiv 5102	1

Syntax hints:  /\wa 369  =wceq 1395  E.wex 1612  e.wcel 1818  <.cop 4035   class class class wbr 4452  o.ccom 5008

This theorem is referenced by:  funcoeqres  5851  fcof1oinvd  6196  tposco  7005  mapen  7701  mapfien  7887  mapfienOLD  8159  hashfacen  12503  cofuass  15258  setccatid  15411  frmdup3lem  16034  symggrp  16425  f1omvdco2  16473  symggen  16495  psgnunilem1  16518  gsumval3OLD  16908  gsumval3  16911  gsumzf1o  16917  gsumzf1oOLD  16920  gsumzmhm  16957  gsumzmhmOLD  16958  prds1  17263  psrass1lem  18029  pf1mpf  18388  pf1ind  18391  qtophmeo  20318  uniioombllem2  21992  cncombf  22065  motgrp  23930  pjsdi2i  27076  pjadj2coi  27123  pj3lem1  27125  pj3i  27127  fcoinver  27460  fcobij  27548  fcobijfs  27549  derangenlem  28615  subfacp1lem5  28628  erdsze2lem2  28648  relexpsucl  29055  relexpadd  29061  pprodcnveq  29533  cocnv  30216  diophrw  30692  eldioph2  30695  mendring  31141  estrccatid  32638  rngccatidOLD  32797  ringccatidOLD  32860  ltrncoidN  35852  trlcoabs2N  36448  trlcoat  36449  trlcone  36454  cdlemg46  36461  cdlemg47  36462  ltrnco4  36465  tgrpgrplem  36475  tendoplass  36509  cdlemi2  36545  cdlemk2  36558  cdlemk4  36560  cdlemk8  36564  cdlemk45  36673  cdlemk54  36684  cdlemk55a  36685  erngdvlem3  36716  erngdvlem3-rN  36724  tendocnv  36748  dvhvaddass  36824  dvhlveclem  36835  cdlemn8  36931  dihopelvalcpre  36975  dih1dimatlem0  37055

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-9 1822  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435  ax-sep 4573  ax-nul 4581  ax-pr 4691

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-eu 2286  df-mo 2287  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-rab 2816  df-v 3111  df-dif 3478  df-un 3480  df-in 3482  df-ss 3489  df-nul 3785  df-if 3942  df-sn 4030  df-pr 4032  df-op 4036  df-br 4453  df-opab 4511  df-xp 5010  df-rel 5011  df-co 5013