Definition df-ref 5901

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

Assertion

Ref	Expression
df-ref	|- Ref = {<.r, a>. | A.x e. a xrx}

Distinct variable group:   r,a,x

Detailed syntax breakdown of Definition df-ref

Step	Hyp	Ref	Expression
1		cref 5890	. 2 class Ref
2		vx	. . . . . 6 setvar x
3	2	cv 1641	. . . . 5 class x
4		vr	. . . . . 6 setvar r
5	4	cv 1641	. . . . 5 class r
6	3, 3, 5	wbr 4640	. . . 4 wff xrx
7		va	. . . . 5 setvar a
8	7	cv 1641	. . . 4 class a
9	6, 2, 8	wral 2615	. . 3 wff A.x e. a xrx
10	9, 4, 7	copab 4623	. 2 class {<.r, a>. | A.x e. a xrx}
11	1, 10	wceq 1642	1 wff Ref = {<.r, a>. | A.x e. a xrx}

This definition is referenced by:  refex  5912  refrd  5927  refd  5928