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 5633
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7765. (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 5630 . 2 wff 𝑅 We 𝐴
41, 2wfr 5628 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5587 . . 3 wff 𝑅 Or 𝐴
64, 5wa 395 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 205 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5652  wess  5663  weeq1  5664  weeq2  5665  wefr  5666  weso  5667  we0  5671  weinxp  5760  wesn  5764  isowe  7349  isowe2  7350  dfwe2  7765  epweon  7766  wexp  8121  wofi  9298  dford5reg  35224  finorwe  36727  fin2so  36939
  Copyright terms: Public domain W3C validator