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 5219
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7138. (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 5216 . 2 wff 𝑅 We 𝐴
41, 2wfr 5214 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5178 . . 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  5234  wess  5245  weeq1  5246  weeq2  5247  wefr  5248  weso  5249  we0  5253  weinxp  5335  wesn  5339  isowe  6754  isowe2  6755  dfwe2  7138  wexp  7451  wofi  8366  dford5reg  31984  fin2so  33701
  Copyright terms: Public domain W3C validator