MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-fr Unicode version

Definition df-fr 4843
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4849 and dffr3 5374. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-fr
Distinct variable groups:   , , ,   , , ,

Detailed syntax breakdown of Definition df-fr
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2wfr 4840 . 2
4 vx . . . . . . 7
54cv 1394 . . . . . 6
65, 1wss 3475 . . . . 5
7 c0 3784 . . . . . 6
85, 7wne 2652 . . . . 5
96, 8wa 369 . . . 4
10 vz . . . . . . . . 9
1110cv 1394 . . . . . . . 8
12 vy . . . . . . . . 9
1312cv 1394 . . . . . . . 8
1411, 13, 2wbr 4452 . . . . . . 7
1514wn 3 . . . . . 6
1615, 10, 5wral 2807 . . . . 5
1716, 12, 5wrex 2808 . . . 4
189, 17wi 4 . . 3
1918, 4wal 1393 . 2
203, 19wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  fri  4846  dffr2  4849  frss  4851  freq1  4854  nffr  4858  frinxp  5070  frsn  5075  f1oweALT  6784  frxp  6910  frfi  7785  fpwwe2lem12  9040  fpwwe2lem13  9041  dffr5  29182  dfon2lem9  29223  fin2so  30040  fnwe2  30999  bnj1154  34055
  Copyright terms: Public domain W3C validator