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

Definition df-we 4503
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4721. (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 4500 . 2  wff  R  We  A
41, 2wfr 4498 . . 3  wff  R  Fr  A
51, 2wor 4462 . . 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  4518  wess  4529  weeq1  4530  weeq2  4531  wefr  4532  weso  4533  we0  4537  dfwe2  4721  weinxp  4904  wesn  4908  isowe  6028  isowe2  6029  wexp  6419  wofi  7315  dford5reg  25352
  Copyright terms: Public domain W3C validator