Users' Mathboxes Mathbox for Jonathan Ben-Naim < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bnj15 Unicode version

Definition df-bnj15 28718
Description: Define the following predicate:  R is both well-founded and set-like on  A. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.) (New usage is discouraged.)
Assertion
Ref Expression
df-bnj15  |-  ( R 
FrSe  A  <->  ( R  Fr  A  /\  R  Se  A
) )

Detailed syntax breakdown of Definition df-bnj15
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2w-bnj15 28717 . 2  wff  R  FrSe  A
41, 2wfr 4349 . . 3  wff  R  Fr  A
51, 2w-bnj13 28715 . . 3  wff  R  Se  A
64, 5wa 358 . 2  wff  ( R  Fr  A  /\  R  Se  A )
73, 6wb 176 1  wff  ( R 
FrSe  A  <->  ( R  Fr  A  /\  R  Se  A
) )
Colors of variables: wff set class
This definition is referenced by:  bnj93  28895  bnj1177  29036  bnj1364  29058  bnj1417  29071
  Copyright terms: Public domain W3C validator