Definition df-disj 5745

Description: Define the relationship of all disjoint sets. (Contributed by SF, 9-Feb-2015.)

Assertion

Ref	Expression
df-disj	|- Disj = {<.x, y>. | (x i^i y) = (/)}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-disj

Step	Hyp	Ref	Expression
1		cdisj 5744	. 2 class Disj
2		vx	. . . . . 6 setvar x
3	2	cv 1641	. . . . 5 class x
4		vy	. . . . . 6 setvar y
5	4	cv 1641	. . . . 5 class y
6	3, 5	cin 3209	. . . 4 class (x i^i y)
7		c0 3551	. . . 4 class (/)
8	6, 7	wceq 1642	. . 3 wff (x i^i y) = (/)
9	8, 2, 4	copab 4623	. 2 class {<.x, y>. | (x i^i y) = (/)}
10	1, 9	wceq 1642	1 wff Disj = {<.x, y>. | (x i^i y) = (/)}

This definition is referenced by:  brdisjg  5822  disjex  5824