Theorem cnvco 5193

Description: Distributive law of converse over class composition. Theorem 26 of [Suppes] p. 64. (Contributed by NM, 19-Mar-1998.) (Proof shortened by Andrew Salmon, 27-Aug-2011.)

Assertion

Ref	Expression
cnvco

Proof of Theorem cnvco

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

Step	Hyp	Ref	Expression
1		exancom 1671	. . . 4
2		vex 3112	. . . . 5
3		vex 3112	. . . . 5
4	2, 3	brco 5178	. . . 4
5		vex 3112	. . . . . . 7
6	3, 5	brcnv 5190	. . . . . 6
7	5, 2	brcnv 5190	. . . . . 6
8	6, 7	anbi12i 697	. . . . 5
9	8	exbii 1667	. . . 4
10	1, 4, 9	3bitr4i 277	. . 3
11	10	opabbii 4516	. 2
12		df-cnv 5012	. 2
13		df-co 5013	. 2
14	11, 12, 13	3eqtr4i 2496	1

Syntax hints:  /\wa 369  =wceq 1395  E.wex 1612   class class class wbr 4452  {copab 4509  `'ccnv 5003  o.ccom 5008

This theorem is referenced by:  rncoss  5268  rncoeq  5271  dmco  5520  cores2  5525  co01  5527  coi2  5529  relcnvtr  5532  dfdm2  5544  f1co  5795  cofunex2g  6765  fparlem3  6902  fparlem4  6903  supp0cosupp0  6958  imacosupp  6959  fsuppcolem  7880  mapfienOLD  8159  cnvps  15842  gimco  16316  gsumval3OLD  16908  gsumzf1o  16917  gsumzf1oOLD  16920  cnco  19767  ptrescn  20140  qtopcn  20215  hmeoco  20273  cncombf  22065  deg1val  22496  deg1valOLD  22497  fcoinver  27460  ofpreima  27507  mbfmco  28235  eulerpartlemmf  28314  cvmliftmolem1  28726  cvmlift2lem9a  28748  cvmlift2lem9  28756  mclsppslem  28943  relexpcnv  29056  ftc1anclem3  30092  trlcocnv  36446  tendoicl  36522  cdlemk45  36673  cnvtrrel  37782

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-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-cnv 5012  df-co 5013