Definition df-ref 21308

Description: Define the refinement relation. (Contributed by Jeff Hankins, 18-Jan-2010.)

Assertion

Ref	Expression
df-ref	|- Ref = { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }

Distinct variable group:   x, w, y, z

Detailed syntax breakdown of Definition df-ref

Step	Hyp	Ref	Expression
1		cref 21305	. 2 class Ref
2		vy	. . . . . . 7 setvar y
3	2	cv 1482	. . . . . 6 class y
4	3	cuni 4436	. . . . 5 class U. y
5		vx	. . . . . . 7 setvar x
6	5	cv 1482	. . . . . 6 class x
7	6	cuni 4436	. . . . 5 class U. x
8	4, 7	wceq 1483	. . . 4 wff U. y = U. x
9		vz	. . . . . . . 8 setvar z
10	9	cv 1482	. . . . . . 7 class z
11		vw	. . . . . . . 8 setvar w
12	11	cv 1482	. . . . . . 7 class w
13	10, 12	wss 3574	. . . . . 6 wff z C_ w
14	13, 11, 3	wrex 2913	. . . . 5 wff E. w e. y z C_ w
15	14, 9, 6	wral 2912	. . . 4 wff A. z e. x E. w e. y z C_ w
16	8, 15	wa 384	. . 3 wff ( U. y = U. x /\ A. z e. x E. w e. y z C_ w )
17	16, 5, 2	copab 4712	. 2 class { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }
18	1, 17	wceq 1483	1 wff Ref = { <. x , y >. | ( U. y = U. x /\ A. z e. x E. w e. y z C_ w ) }

This definition is referenced by:  refrel  21311  isref  21312