Definition df-frfor 4248

Description: Define the well-founded relation predicate where A might be a proper class. By passing in S we allow it potentially to be a proper class rather than a set. (Contributed by Jim Kingdon and Mario Carneiro, 22-Sep-2021.)

Assertion

Ref	Expression
df-frfor	|- (FrFor R A S <-> ( A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S ) -> A C_ S ) )

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

Detailed syntax breakdown of Definition df-frfor

Step	Hyp	Ref	Expression
1		cA	. . 3 class A
2		cR	. . 3 class R
3		cS	. . 3 class S
4	1, 2, 3	wfrfor 4244	. 2 wff FrFor R A S
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1330	. . . . . . . 8 class y
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1330	. . . . . . . 8 class x
9	6, 8, 2	wbr 3924	. . . . . . 7 wff y R x
10	6, 3	wcel 1480	. . . . . . 7 wff y e. S
11	9, 10	wi 4	. . . . . 6 wff ( y R x -> y e. S )
12	11, 5, 1	wral 2414	. . . . 5 wff A. y e. A ( y R x -> y e. S )
13	8, 3	wcel 1480	. . . . 5 wff x e. S
14	12, 13	wi 4	. . . 4 wff ( A. y e. A ( y R x -> y e. S ) -> x e. S )
15	14, 7, 1	wral 2414	. . 3 wff A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S )
16	1, 3	wss 3066	. . 3 wff A C_ S
17	15, 16	wi 4	. 2 wff ( A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S ) -> A C_ S )
18	4, 17	wb 104	1 wff (FrFor R A S <-> ( A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S ) -> A C_ S ) )

This definition is referenced by:  frforeq1  4260  frforeq2  4262  frforeq3  4264  nffrfor  4265  frirrg  4267  fr0  4268  frind  4269  zfregfr  4483