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

Definition df-we 4355
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4574. (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 4352 . 2  wff  R  We  A
41, 2wfr 4350 . . 3  wff  R  Fr  A
51, 2wor 4314 . . 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  4370  wess  4381  weeq1  4382  weeq2  4383  wefr  4384  weso  4385  we0  4389  dfwe2  4574  weinxp  4758  wesn  4762  isowe  5809  isowe2  5810  wexp  6192  wofi  7103  dford5reg  23541
  Copyright terms: Public domain W3C validator