MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-we Unicode version

Definition df-we 4845
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6617. (Contributed by NM, 3-Apr-1994.)
Assertion
Ref Expression
df-we

Detailed syntax breakdown of Definition df-we
StepHypRef Expression
1 cA . . 3
2 cR . . 3
31, 2wwe 4842 . 2
41, 2wfr 4840 . . 3
51, 2wor 4804 . . 3
64, 5wa 369 . 2
73, 6wb 184 1
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  4860  wess  4871  weeq1  4872  weeq2  4873  wefr  4874  weso  4875  we0  4879  weinxp  5072  wesn  5076  isowe  6245  isowe2  6246  dfwe2  6617  wexp  6914  wofi  7789  dford5reg  29214  fin2so  30040
  Copyright terms: Public domain W3C validator