Definition df-connex 5904

Description: Define the set of all connected relationships over a base set. (Contributed by SF, 19-Feb-2015.)

Assertion

Ref	Expression
df-connex	⊢ Connex = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)}

Distinct variable group:   r,a,x,y

Detailed syntax breakdown of Definition df-connex

Step	Hyp	Ref	Expression
1		cconnex 5893	. 2 class Connex
2		vx	. . . . . . . 8 setvar x
3	2	cv 1641	. . . . . . 7 class x
4		vy	. . . . . . . 8 setvar y
5	4	cv 1641	. . . . . . 7 class y
6		vr	. . . . . . . 8 setvar r
7	6	cv 1641	. . . . . . 7 class r
8	3, 5, 7	wbr 4640	. . . . . 6 wff xry
9	5, 3, 7	wbr 4640	. . . . . 6 wff yrx
10	8, 9	wo 357	. . . . 5 wff (xry ∨ yrx)
11		va	. . . . . 6 setvar a
12	11	cv 1641	. . . . 5 class a
13	10, 4, 12	wral 2615	. . . 4 wff ∀y ∈ a (xry ∨ yrx)
14	13, 2, 12	wral 2615	. . 3 wff ∀x ∈ a ∀y ∈ a (xry ∨ yrx)
15	14, 6, 11	copab 4623	. 2 class {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)}
16	1, 15	wceq 1642	1 wff Connex = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (xry ∨ yrx)}

This definition is referenced by:  connexex  5914  connexrd  5931  connexd  5932