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

Definition df-we 5514
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7487. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-we (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))

Detailed syntax breakdown of Definition df-we
StepHypRef Expression
1 cA . . 3 class 𝐴
2 cR . . 3 class 𝑅
31, 2wwe 5511 . 2 wff 𝑅 We 𝐴
41, 2wfr 5509 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5471 . . 3 wff 𝑅 Or 𝐴
64, 5wa 396 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 207 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5529  wess  5540  weeq1  5541  weeq2  5542  wefr  5543  weso  5544  we0  5548  weinxp  5634  wesn  5638  isowe  7097  isowe2  7098  dfwe2  7487  wexp  7818  wofi  8759  dford5reg  32911  finorwe  34532  fin2so  34746
  Copyright terms: Public domain W3C validator