Definition df-co 4727

Description: Define the composition of two classes. (Contributed by SF, 5-Jan-2015.)

Assertion

Ref	Expression
df-co	⊢ (A ∘ B) = {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}

Distinct variable groups:   x,A,y,z   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 4722	. 2 class (A ∘ B)
4		vx	. . . . . . 7 setvar x
5	4	cv 1641	. . . . . 6 class x
6		vz	. . . . . . 7 setvar z
7	6	cv 1641	. . . . . 6 class z
8	5, 7, 2	wbr 4640	. . . . 5 wff xBz
9		vy	. . . . . . 7 setvar y
10	9	cv 1641	. . . . . 6 class y
11	7, 10, 1	wbr 4640	. . . . 5 wff zAy
12	8, 11	wa 358	. . . 4 wff (xBz ∧ zAy)
13	12, 6	wex 1541	. . 3 wff ∃z(xBz ∧ zAy)
14	13, 4, 9	copab 4623	. 2 class {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}
15	3, 14	wceq 1642	1 wff (A ∘ B) = {⟨x, y⟩ ∣ ∃z(xBz ∧ zAy)}

This definition is referenced by:  dfco1  4749  coss1  4873  coss2  4874  nfco  4883  brco  4884  cnvco  4895  coundi  5083  coundir  5084  cores  5085  df2nd2  5112  funco  5143  composeex  5821