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

Definition df-fr 4245
Description: Define the well-founded relation predicate. Definition 6.24(1) of [TakeutiZaring] p. 30. For alternate definitions, see dffr2 4251 and dffr3 4952. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-fr  |-  ( R  Fr  A  <->  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
Distinct variable groups:    x, y,
z, R    x, A, y, z

Detailed syntax breakdown of Definition df-fr
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wfr 4242 . 2  wff  R  Fr  A
4 vx . . . . . . 7  set  x
54cv 1618 . . . . . 6  class  x
65, 1wss 3078 . . . . 5  wff  x  C_  A
7 c0 3362 . . . . . 6  class  (/)
85, 7wne 2412 . . . . 5  wff  x  =/=  (/)
96, 8wa 360 . . . 4  wff  ( x 
C_  A  /\  x  =/=  (/) )
10 vz . . . . . . . . 9  set  z
1110cv 1618 . . . . . . . 8  class  z
12 vy . . . . . . . . 9  set  y
1312cv 1618 . . . . . . . 8  class  y
1411, 13, 2wbr 3920 . . . . . . 7  wff  z R y
1514wn 5 . . . . . 6  wff  -.  z R y
1615, 10, 5wral 2509 . . . . 5  wff  A. z  e.  x  -.  z R y
1716, 12, 5wrex 2510 . . . 4  wff  E. y  e.  x  A. z  e.  x  -.  z R y
189, 17wi 6 . . 3  wff  ( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
1918, 4wal 1532 . 2  wff  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y )
203, 19wb 178 1  wff  ( R  Fr  A  <->  A. x
( ( x  C_  A  /\  x  =/=  (/) )  ->  E. y  e.  x  A. z  e.  x  -.  z R y ) )
Colors of variables: wff set class
This definition is referenced by:  fri  4248  dffr2  4251  frss  4253  freq1  4256  nffr  4260  frinxp  4662  frsn  4667  f1oweALT  5703  frxp  6077  frfi  6987  fpwwe2lem12  8143  fpwwe2lem13  8144  dffr5  23280  dfon2lem9  23315  fnwe2  26316  bnj1154  27718
  Copyright terms: Public domain W3C validator