Definition df-co 4612

Description: Define the composition of two classes. Definition 6.6(3) of [TakeutiZaring] p. 24. Note that Definition 7 of [Suppes] p. 63 reverses A and B, uses a slash instead of o., and calls the operation "relative product". (Contributed by NM, 4-Jul-1994.)

Assertion

Ref	Expression
df-co	|- ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }

Distinct variable groups:   x, y, z, A   x, B, y, z

Detailed syntax breakdown of Definition df-co

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cB	. . 3 class B
3	1, 2	ccom 4607	. 2 class ( A o. B )
4		vx	. . . . . . 7 setvar x
5	4	cv 1342	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1342	. . . . . 6 class z
8	5, 7, 2	wbr 3981	. . . . 5 wff x B z
9		vy	. . . . . . 7 setvar y
10	9	cv 1342	. . . . . 6 class y
11	7, 10, 1	wbr 3981	. . . . 5 wff z A y
12	8, 11	wa 103	. . . 4 wff ( x B z /\ z A y )
13	12, 6	wex 1480	. . 3 wff E. z ( x B z /\ z A y )
14	13, 4, 9	copab 4041	. 2 class { <. x , y >. | E. z ( x B z /\ z A y ) }
15	3, 14	wceq 1343	1 wff ( A o. B ) = { <. x , y >. | E. z ( x B z /\ z A y ) }

This definition is referenced by:  coss1  4758  coss2  4759  nfco  4768  elco  4769  brcog  4770  cnvco  4788  cotr  4984  relco  5101  coundi  5104  coundir  5105  cores  5106  xpcom  5149  dffun2  5197  funco  5227  xpcomco  6788