Definition df-frfor 4068

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 4064	. 2 wff FrFor 𝑅𝐴𝑆
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1242	. . . . . . . 8 class 𝑦
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1242	. . . . . . . 8 class 𝑥
9	6, 8, 2	wbr 3764	. . . . . . 7 wff 𝑦𝑅𝑥
10	6, 3	wcel 1393	. . . . . . 7 wff 𝑦 ∈ 𝑆
11	9, 10	wi 4	. . . . . 6 wff (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆)
12	11, 5, 1	wral 2306	. . . . 5 wff ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆)
13	8, 3	wcel 1393	. . . . 5 wff 𝑥 ∈ 𝑆
14	12, 13	wi 4	. . . 4 wff (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
15	14, 7, 1	wral 2306	. . 3 wff ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
16	1, 3	wss 2917	. . 3 wff 𝐴 ⊆ 𝑆
17	15, 16	wi 4	. 2 wff (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)
18	4, 17	wb 98	1 wff ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))

This definition is referenced by:  frforeq1  4080  frforeq2  4082  frforeq3  4084  nffrfor  4085  frirrg  4087  fr0  4088  frind  4089  zfregfr  4298