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 5045
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6943. (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 5042 . 2 wff 𝑅 We 𝐴
41, 2wfr 5040 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5004 . . 3 wff 𝑅 Or 𝐴
64, 5wa 384 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 196 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5060  wess  5071  weeq1  5072  weeq2  5073  wefr  5074  weso  5075  we0  5079  weinxp  5157  wesn  5161  isowe  6564  isowe2  6565  dfwe2  6943  wexp  7251  wofi  8169  dford5reg  31441  fin2so  33067
  Copyright terms: Public domain W3C validator