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

Definition df-we 4486
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4704. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-we  |-  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )

Detailed syntax breakdown of Definition df-we
StepHypRef Expression
1 cA . . 3  class  A
2 cR . . 3  class  R
31, 2wwe 4483 . 2  wff  R  We  A
41, 2wfr 4481 . . 3  wff  R  Fr  A
51, 2wor 4445 . . 3  wff  R  Or  A
64, 5wa 359 . 2  wff  ( R  Fr  A  /\  R  Or  A )
73, 6wb 177 1  wff  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
Colors of variables: wff set class
This definition is referenced by:  nfwe  4501  wess  4512  weeq1  4513  weeq2  4514  wefr  4515  weso  4516  we0  4520  dfwe2  4704  weinxp  4887  wesn  4891  isowe  6010  isowe2  6011  wexp  6398  wofi  7294  dford5reg  25164
  Copyright terms: Public domain W3C validator