Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-frfor Unicode version

Definition df-frfor 4248
 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
StepHypRef Expression
1 cA . . 3
2 cR . . 3
3 cS . . 3
41, 2, 3wfrfor 4244 . 2 FrFor
5 vy . . . . . . . . 9
65cv 1330 . . . . . . . 8
7 vx . . . . . . . . 9
87cv 1330 . . . . . . . 8
96, 8, 2wbr 3924 . . . . . . 7
106, 3wcel 1480 . . . . . . 7
119, 10wi 4 . . . . . 6
1211, 5, 1wral 2414 . . . . 5
138, 3wcel 1480 . . . . 5
1412, 13wi 4 . . . 4
1514, 7, 1wral 2414 . . 3
161, 3wss 3066 . . 3
1715, 16wi 4 . 2
184, 17wb 104 1 FrFor
 Colors of variables: wff set class This definition is referenced by:  frforeq1  4260  frforeq2  4262  frforeq3  4264  nffrfor  4265  frirrg  4267  fr0  4268  frind  4269  zfregfr  4483
 Copyright terms: Public domain W3C validator