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

Definition df-found 5905
 Description: Define the set of all founded relationships over a base set. (Contributed by SF, 19-Feb-2015.)
Assertion
Ref Expression
df-found Fr = {r, a x((x a x) → z x y x (yrzy = z))}
Distinct variable group:   r,a,x,y,z

Detailed syntax breakdown of Definition df-found
StepHypRef Expression
1 cfound 5894 . 2 class Fr
2 vx . . . . . . . 8 setvar x
32cv 1641 . . . . . . 7 class x
4 va . . . . . . . 8 setvar a
54cv 1641 . . . . . . 7 class a
63, 5wss 3257 . . . . . 6 wff x a
7 c0 3550 . . . . . . 7 class
83, 7wne 2516 . . . . . 6 wff x
96, 8wa 358 . . . . 5 wff (x a x)
10 vy . . . . . . . . . 10 setvar y
1110cv 1641 . . . . . . . . 9 class y
12 vz . . . . . . . . . 10 setvar z
1312cv 1641 . . . . . . . . 9 class z
14 vr . . . . . . . . . 10 setvar r
1514cv 1641 . . . . . . . . 9 class r
1611, 13, 15wbr 4639 . . . . . . . 8 wff yrz
1710, 12weq 1643 . . . . . . . 8 wff y = z
1816, 17wi 4 . . . . . . 7 wff (yrzy = z)
1918, 10, 3wral 2614 . . . . . 6 wff y x (yrzy = z)
2019, 12, 3wrex 2615 . . . . 5 wff z x y x (yrzy = z)
219, 20wi 4 . . . 4 wff ((x a x) → z x y x (yrzy = z))
2221, 2wal 1540 . . 3 wff x((x a x) → z x y x (yrzy = z))
2322, 14, 4copab 4622 . 2 class {r, a x((x a x) → z x y x (yrzy = z))}
241, 23wceq 1642 1 wff Fr = {r, a x((x a x) → z x y x (yrzy = z))}
 Colors of variables: wff setvar class This definition is referenced by:  foundex  5914  frd  5922
 Copyright terms: Public domain W3C validator