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 5485
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7515. (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 5482 . 2 wff 𝑅 We 𝐴
41, 2wfr 5480 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5441 . . 3 wff 𝑅 Or 𝐴
64, 5wa 399 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 209 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5501  wess  5512  weeq1  5513  weeq2  5514  wefr  5515  weso  5516  we0  5520  weinxp  5607  wesn  5611  isowe  7115  isowe2  7116  dfwe2  7515  wexp  7850  wofi  8841  dford5reg  33330  finorwe  35176  fin2so  35387
  Copyright terms: Public domain W3C validator