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 5639
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7794. (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 5636 . 2 wff 𝑅 We 𝐴
41, 2wfr 5634 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5591 . . 3 wff 𝑅 Or 𝐴
64, 5wa 395 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 206 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5660  wess  5671  weeq1  5672  weeq2  5673  wefr  5675  weso  5676  we0  5680  weinxp  5770  wesn  5774  isowe  7369  isowe2  7370  dfwe2  7794  epweon  7795  wexp  8155  wofi  9325  dford5reg  35783  weiunwe  36470  finorwe  37383  fin2so  37614
  Copyright terms: Public domain W3C validator