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

Definition df-frind 4095
 Description: Define the well-founded relation predicate. In the presence of excluded middle, there are a variety of equivalent ways to define this. In our case, this definition, in terms of an inductive principle, works better than one along the lines of "there is an element which is minimal when A is ordered by R". Because is constrained to be a set (not a proper class) here, sometimes it may be necessary to use FrFor directly rather than via . (Contributed by Jim Kingdon and Mario Carneiro, 21-Sep-2021.)
Assertion
Ref Expression
df-frind FrFor
Distinct variable groups:   ,   ,

Detailed syntax breakdown of Definition df-frind
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2wfr 4091 . 2
4 vs . . . . 5
54cv 1284 . . . 4
61, 2, 5wfrfor 4090 . . 3 FrFor
76, 4wal 1283 . 2 FrFor
83, 7wb 103 1 FrFor
 Colors of variables: wff set class This definition is referenced by:  freq1  4107  freq2  4109  nffr  4112  frirrg  4113  fr0  4114  frind  4115  zfregfr  4324
 Copyright terms: Public domain W3C validator