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 4988
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6850. (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 4985 . 2 wff 𝑅 We 𝐴
41, 2wfr 4983 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 4947 . . 3 wff 𝑅 Or 𝐴
64, 5wa 382 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 194 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5003  wess  5014  weeq1  5015  weeq2  5016  wefr  5017  weso  5018  we0  5022  weinxp  5098  wesn  5102  isowe  6476  isowe2  6477  dfwe2  6850  wexp  7155  wofi  8071  dford5reg  30724  fin2so  32349
  Copyright terms: Public domain W3C validator