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

Definition df-we 4312
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4531. (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 4309 . 2  wff  R  We  A
41, 2wfr 4307 . . 3  wff  R  Fr  A
51, 2wor 4271 . . 3  wff  R  Or  A
64, 5wa 360 . 2  wff  ( R  Fr  A  /\  R  Or  A )
73, 6wb 178 1  wff  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
Colors of variables: wff set class
This definition is referenced by:  nfwe  4327  wess  4338  weeq1  4339  weeq2  4340  wefr  4341  weso  4342  we0  4346  dfwe2  4531  weinxp  4731  wesn  4735  isowe  5766  isowe2  5767  wexp  6149  wofi  7060  dford5reg  23493
  Copyright terms: Public domain W3C validator