NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-antisym Unicode version

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
Distinct variable group:   ,,,

Detailed syntax breakdown of Definition df-antisym
StepHypRef Expression
1 cantisym 5890 . 2 Antisym
2 vx . . . . . . . . 9
32cv 1641 . . . . . . . 8
4 vy . . . . . . . . 9
54cv 1641 . . . . . . . 8
6 vr . . . . . . . . 9
76cv 1641 . . . . . . . 8
83, 5, 7wbr 4639 . . . . . . 7
95, 3, 7wbr 4639 . . . . . . 7
108, 9wa 358 . . . . . 6
112, 4weq 1643 . . . . . 6
1210, 11wi 4 . . . . 5
13 va . . . . . 6
1413cv 1641 . . . . 5
1512, 4, 14wral 2614 . . . 4
1615, 2, 14wral 2614 . . 3
1716, 6, 13copab 4622 . 2
181, 17wceq 1642 1 Antisym
Colors of variables: wff setvar class
This definition is referenced by:  antisymex  5912  antird  5928  antid  5929
  Copyright terms: Public domain W3C validator