Definition df-frfor 4333

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 4329	. 2 wff FrFor R A S
5		vy	. . . . . . . . 9 setvar y
6	5	cv 1352	. . . . . . . 8 class y
7		vx	. . . . . . . . 9 setvar x
8	7	cv 1352	. . . . . . . 8 class x
9	6, 8, 2	wbr 4005	. . . . . . 7 wff y R x
10	6, 3	wcel 2148	. . . . . . 7 wff y e. S
11	9, 10	wi 4	. . . . . 6 wff ( y R x -> y e. S )
12	11, 5, 1	wral 2455	. . . . 5 wff A. y e. A ( y R x -> y e. S )
13	8, 3	wcel 2148	. . . . 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 2455	. . 3 wff A. x e. A ( A. y e. A ( y R x -> y e. S ) -> x e. S )
16	1, 3	wss 3131	. . 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 105	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  4345  frforeq2  4347  frforeq3  4349  nffrfor  4350  frirrg  4352  fr0  4353  frind  4354  zfregfr  4575