Definition df-ext 5908

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⟩ ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ 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 5897	. 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 4640	. . . . . . . 8 wff zrx
9		vy	. . . . . . . . . 10 setvar y
10	9	cv 1641	. . . . . . . . 9 class y
11	3, 10, 7	wbr 4640	. . . . . . . 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 2615	. . . . . 6 wff ∀z ∈ a (zrx ↔ zry)
16	4, 9	weq 1643	. . . . . 6 wff x = y
17	15, 16	wi 4	. . . . 5 wff (∀z ∈ a (zrx ↔ zry) → x = y)
18	17, 9, 14	wral 2615	. . . 4 wff ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)
19	18, 4, 14	wral 2615	. . 3 wff ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)
20	19, 6, 13	copab 4623	. 2 class {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)}
21	1, 20	wceq 1642	1 wff Ext = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a (∀z ∈ a (zrx ↔ zry) → x = y)}

This definition is referenced by:  extex  5916  extd  5924