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

Definition df-we 4370
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4589. (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 4367 . 2  wff  R  We  A
41, 2wfr 4365 . . 3  wff  R  Fr  A
51, 2wor 4329 . . 3  wff  R  Or  A
64, 5wa 358 . 2  wff  ( R  Fr  A  /\  R  Or  A )
73, 6wb 176 1  wff  ( R  We  A  <->  ( R  Fr  A  /\  R  Or  A ) )
Colors of variables: wff set class
This definition is referenced by:  nfwe  4385  wess  4396  weeq1  4397  weeq2  4398  wefr  4399  weso  4400  we0  4404  dfwe2  4589  weinxp  4773  wesn  4777  isowe  5862  isowe2  5863  wexp  6245  wofi  7122  dford5reg  24208
  Copyright terms: Public domain W3C validator