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

Definition df-fr 4796
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4802 and dffr3 5320. (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 4793 . 2
4 vx . . . . . . 7
54cv 1369 . . . . . 6
65, 1wss 3442 . . . . 5
7 c0 3751 . . . . . 6
85, 7wne 2648 . . . . 5
96, 8wa 369 . . . 4
10 vz . . . . . . . . 9
1110cv 1369 . . . . . . . 8
12 vy . . . . . . . . 9
1312cv 1369 . . . . . . . 8
1411, 13, 2wbr 4409 . . . . . . 7
1514wn 3 . . . . . 6
1615, 10, 5wral 2800 . . . . 5
1716, 12, 5wrex 2801 . . . 4
189, 17wi 4 . . 3
1918, 4wal 1368 . 2
203, 19wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  fri  4799  dffr2  4802  frss  4804  freq1  4807  nffr  4811  frinxp  5021  frsn  5026  f1oweALT  6694  frxp  6816  frfi  7692  fpwwe2lem12  8945  fpwwe2lem13  8946  dffr5  28019  dfon2lem9  28060  fin2so  28876  fnwe2  29866  bnj1154  32833
  Copyright terms: Public domain W3C validator