Definition df-frfor 4366

Description: Define the well-founded relation predicate where 𝐴 might be a proper class. By passing in 𝑆 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 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))

Distinct variable groups:   𝑥,𝑦,𝑅   𝑥,𝐴,𝑦   𝑥,𝑆,𝑦

Detailed syntax breakdown of Definition df-frfor

Step	Hyp	Ref	Expression
1		cA	. . 3 class 𝐴
2		cR	. . 3 class 𝑅
3		cS	. . 3 class 𝑆
4	1, 2, 3	wfrfor 4362	. 2 wff FrFor 𝑅𝐴𝑆
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1363	. . . . . . . 8 class 𝑦
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1363	. . . . . . . 8 class 𝑥
9	6, 8, 2	wbr 4033	. . . . . . 7 wff 𝑦𝑅𝑥
10	6, 3	wcel 2167	. . . . . . 7 wff 𝑦 ∈ 𝑆
11	9, 10	wi 4	. . . . . 6 wff (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆)
12	11, 5, 1	wral 2475	. . . . 5 wff ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆)
13	8, 3	wcel 2167	. . . . 5 wff 𝑥 ∈ 𝑆
14	12, 13	wi 4	. . . 4 wff (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
15	14, 7, 1	wral 2475	. . 3 wff ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
16	1, 3	wss 3157	. . 3 wff 𝐴 ⊆ 𝑆
17	15, 16	wi 4	. 2 wff (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)
18	4, 17	wb 105	1 wff ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))

This definition is referenced by:  frforeq1  4378  frforeq2  4380  frforeq3  4382  nffrfor  4383  frirrg  4385  fr0  4386  frind  4387  zfregfr  4610