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

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

Detailed syntax breakdown of Definition df-ext
StepHypRef Expression
1 cext 5896 . 2 Ext
2 vz . . . . . . . . . 10
32cv 1641 . . . . . . . . 9
4 vx . . . . . . . . . 10
54cv 1641 . . . . . . . . 9
6 vr . . . . . . . . . 10
76cv 1641 . . . . . . . . 9
83, 5, 7wbr 4639 . . . . . . . 8
9 vy . . . . . . . . . 10
109cv 1641 . . . . . . . . 9
113, 10, 7wbr 4639 . . . . . . . 8
128, 11wb 176 . . . . . . 7
13 va . . . . . . . 8
1413cv 1641 . . . . . . 7
1512, 2, 14wral 2614 . . . . . 6
164, 9weq 1643 . . . . . 6
1715, 16wi 4 . . . . 5
1817, 9, 14wral 2614 . . . 4
1918, 4, 14wral 2614 . . 3
2019, 6, 13copab 4622 . 2
211, 20wceq 1642 1 Ext
 Colors of variables: wff setvar class This definition is referenced by:  extex  5915  extd  5923
 Copyright terms: Public domain W3C validator