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 ∩ 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 ∩ y)
7		c0 3551	. . . 4 class ∅
8	6, 7	wceq 1642	. . 3 wff (x ∩ y) = ∅
9	8, 2, 4	copab 4623	. 2 class {⟨x, y⟩ ∣ (x ∩ y) = ∅}
10	1, 9	wceq 1642	1 wff Disj = {⟨x, y⟩ ∣ (x ∩ y) = ∅}

This definition is referenced by:  brdisjg  5822  disjex  5824