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

Definition df-we 4545
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4764. (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 4542 . 2  wff  R  We  A
41, 2wfr 4540 . . 3  wff  R  Fr  A
51, 2wor 4504 . . 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  4560  wess  4571  weeq1  4572  weeq2  4573  wefr  4574  weso  4575  we0  4579  dfwe2  4764  weinxp  4947  wesn  4951  isowe  6071  isowe2  6072  wexp  6462  wofi  7358  dford5reg  25411
  Copyright terms: Public domain W3C validator