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 4999
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6873. (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 4996 . 2 wff 𝑅 We 𝐴
41, 2wfr 4994 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 4958 . . 3 wff 𝑅 Or 𝐴
64, 5wa 383 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 195 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5014  wess  5025  weeq1  5026  weeq2  5027  wefr  5028  weso  5029  we0  5033  weinxp  5109  wesn  5113  isowe  6499  isowe2  6500  dfwe2  6873  wexp  7178  wofi  8094  dford5reg  30931  fin2so  32566
  Copyright terms: Public domain W3C validator