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 5104
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7023. (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 5101 . 2 wff 𝑅 We 𝐴
41, 2wfr 5099 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5063 . . 3 wff 𝑅 Or 𝐴
64, 5wa 383 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 196 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5119  wess  5130  weeq1  5131  weeq2  5132  wefr  5133  weso  5134  we0  5138  weinxp  5220  wesn  5224  isowe  6639  isowe2  6640  dfwe2  7023  wexp  7336  wofi  8250  dford5reg  31811  fin2so  33526
  Copyright terms: Public domain W3C validator