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 5510
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7484. (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 5507 . 2 wff 𝑅 We 𝐴
41, 2wfr 5505 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5467 . . 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  5525  wess  5536  weeq1  5537  weeq2  5538  wefr  5539  weso  5540  we0  5544  weinxp  5630  wesn  5634  isowe  7091  isowe2  7092  dfwe2  7484  wexp  7815  wofi  8756  dford5reg  32925  finorwe  34546  fin2so  34761
  Copyright terms: Public domain W3C validator