Definition df-ext 5907

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

Assertion

Ref	Expression
df-ext	|- Ext = {<.r, a>. | A.x e. a A.y e. a (A.z e. a (zrx <-> zry) -> x = y)}

Distinct variable group:   r,a,x,y,z

Detailed syntax breakdown of Definition df-ext

Step	Hyp	Ref	Expression
1		cext 5896	. 2 class Ext
2		vz	. . . . . . . . . 10 setvar z
3	2	cv 1641	. . . . . . . . 9 class z
4		vx	. . . . . . . . . 10 setvar x
5	4	cv 1641	. . . . . . . . 9 class x
6		vr	. . . . . . . . . 10 setvar r
7	6	cv 1641	. . . . . . . . 9 class r
8	3, 5, 7	wbr 4639	. . . . . . . 8 wff zrx
9		vy	. . . . . . . . . 10 setvar y
10	9	cv 1641	. . . . . . . . 9 class y
11	3, 10, 7	wbr 4639	. . . . . . . 8 wff zry
12	8, 11	wb 176	. . . . . . 7 wff (zrx <-> zry)
13		va	. . . . . . . 8 setvar a
14	13	cv 1641	. . . . . . 7 class a
15	12, 2, 14	wral 2614	. . . . . 6 wff A.z e. a (zrx <-> zry)
16	4, 9	weq 1643	. . . . . 6 wff x = y
17	15, 16	wi 4	. . . . 5 wff (A.z e. a (zrx <-> zry) -> x = y)
18	17, 9, 14	wral 2614	. . . 4 wff A.y e. a (A.z e. a (zrx <-> zry) -> x = y)
19	18, 4, 14	wral 2614	. . 3 wff A.x e. a A.y e. a (A.z e. a (zrx <-> zry) -> x = y)
20	19, 6, 13	copab 4622	. 2 class {<.r, a>. | A.x e. a A.y e. a (A.z e. a (zrx <-> zry) -> x = y)}
21	1, 20	wceq 1642	1 wff Ext = {<.r, a>. | A.x e. a A.y e. a (A.z e. a (zrx <-> zry) -> x = y)}

This definition is referenced by:  extex  5915  extd  5923