NFE Home New Foundations Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  NFE Home  >  Th. List  >  df-ext GIF 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 = {r, a x a y a (z a (zrxzry) → x = y)}
Distinct variable group:   r,a,x,y,z

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