Definition df-frfor 4316

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 4312	. 2 wff FrFor 𝑅𝐴𝑆
5		vy	. . . . . . . . 9 setvar 𝑦
6	5	cv 1347	. . . . . . . 8 class 𝑦
7		vx	. . . . . . . . 9 setvar 𝑥
8	7	cv 1347	. . . . . . . 8 class 𝑥
9	6, 8, 2	wbr 3989	. . . . . . 7 wff 𝑦𝑅𝑥
10	6, 3	wcel 2141	. . . . . . 7 wff 𝑦 ∈ 𝑆
11	9, 10	wi 4	. . . . . 6 wff (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆)
12	11, 5, 1	wral 2448	. . . . 5 wff ∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆)
13	8, 3	wcel 2141	. . . . 5 wff 𝑥 ∈ 𝑆
14	12, 13	wi 4	. . . 4 wff (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
15	14, 7, 1	wral 2448	. . 3 wff ∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆)
16	1, 3	wss 3121	. . 3 wff 𝐴 ⊆ 𝑆
17	15, 16	wi 4	. 2 wff (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆)
18	4, 17	wb 104	1 wff ( FrFor 𝑅𝐴𝑆 ↔ (∀𝑥 ∈ 𝐴 (∀𝑦 ∈ 𝐴 (𝑦𝑅𝑥 → 𝑦 ∈ 𝑆) → 𝑥 ∈ 𝑆) → 𝐴 ⊆ 𝑆))

This definition is referenced by:  frforeq1  4328  frforeq2  4330  frforeq3  4332  nffrfor  4333  frirrg  4335  fr0  4336  frind  4337  zfregfr  4558