Definition df-fr 3625

Description: Define the founded relation predicate. For alternate definitions, see dffr2 3627 and dffr3 4297.

Assertion

Ref	Expression
df-fr	|- (R Fr A <-> A.x((x C_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))

Distinct variable groups:   x,y,z,R   x,A,y,z

Detailed syntax breakdown of Definition df-fr

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3	1, 2	wfr 3623	. 2 wff R Fr A
4		vx	. . . . . . 7 set x
5	4	cv 1297	. . . . . 6 class x
6	5, 1	wss 2593	. . . . 5 wff x C_ A
7		c0 2875	. . . . . 6 class (/)
8	5, 7	wne 2017	. . . . 5 wff x =/= (/)
9	6, 8	wa 240	. . . 4 wff (x C_ A /\ x =/= (/))
10		vz	. . . . . . . . 9 set z
11	10	cv 1297	. . . . . . . 8 class z
12		vy	. . . . . . . . 9 set y
13	12	cv 1297	. . . . . . . 8 class y
14	11, 13, 2	wbr 3338	. . . . . . 7 wff zRy
15	14	wn 2	. . . . . 6 wff -. zRy
16	15, 10, 5	wral 2105	. . . . 5 wff A.z e. x -. zRy
17	16, 12, 5	wrex 2106	. . . 4 wff E.y e. x A.z e. x -. zRy
18	9, 17	wi 3	. . 3 wff ((x C_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy)
19	18, 4	wal 1296	. 2 wff A.x((x C_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy)
20	3, 19	wb 163	1 wff (R Fr A <-> A.x((x C_ A /\ x =/= (/)) -> E.y e. x A.z e. x -. zRy))

This definition is referenced by:  fri 3626  dffr2 3627  dffr2OLD 3628  frss 3630  freq1 3632  weinxp 4059  f1oweALT 4883  bnj1154 13438  dffr5 13831  dfon2lem9 13857  frxp 13951  wofi 15770  frfi 15771

Copyright terms: Public domain