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 5272
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 7207. (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 5269 . 2 wff 𝑅 We 𝐴
41, 2wfr 5267 . . 3 wff 𝑅 Fr 𝐴
51, 2wor 5231 . . 3 wff 𝑅 Or 𝐴
64, 5wa 384 . 2 wff (𝑅 Fr 𝐴𝑅 Or 𝐴)
73, 6wb 197 1 wff (𝑅 We 𝐴 ↔ (𝑅 Fr 𝐴𝑅 Or 𝐴))
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  5287  wess  5298  weeq1  5299  weeq2  5300  wefr  5301  weso  5302  we0  5306  weinxp  5388  wesn  5392  isowe  6819  isowe2  6820  dfwe2  7207  wexp  7521  wofi  8444  dford5reg  32002  fin2so  33704
  Copyright terms: Public domain W3C validator