Definition df-antisym 5901

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

Assertion

Ref	Expression
df-antisym	⊢ Antisym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)}

Distinct variable group:   r,a,x,y

Detailed syntax breakdown of Definition df-antisym

Step	Hyp	Ref	Expression
1		cantisym 5890	. 2 class Antisym
2		vx	. . . . . . . . 9 setvar x
3	2	cv 1641	. . . . . . . 8 class x
4		vy	. . . . . . . . 9 setvar y
5	4	cv 1641	. . . . . . . 8 class y
6		vr	. . . . . . . . 9 setvar r
7	6	cv 1641	. . . . . . . 8 class r
8	3, 5, 7	wbr 4639	. . . . . . 7 wff xry
9	5, 3, 7	wbr 4639	. . . . . . 7 wff yrx
10	8, 9	wa 358	. . . . . 6 wff (xry ∧ yrx)
11	2, 4	weq 1643	. . . . . 6 wff x = y
12	10, 11	wi 4	. . . . 5 wff ((xry ∧ yrx) → x = y)
13		va	. . . . . 6 setvar a
14	13	cv 1641	. . . . 5 class a
15	12, 4, 14	wral 2614	. . . 4 wff ∀y ∈ a ((xry ∧ yrx) → x = y)
16	15, 2, 14	wral 2614	. . 3 wff ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)
17	16, 6, 13	copab 4622	. 2 class {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)}
18	1, 17	wceq 1642	1 wff Antisym = {⟨r, a⟩ ∣ ∀x ∈ a ∀y ∈ a ((xry ∧ yrx) → x = y)}

This definition is referenced by:  antisymex  5912  antird  5928  antid  5929