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

Definition df-we 4684
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6358. (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 4681 . 2
41, 2wfr 4679 . . 3
51, 2wor 4643 . . 3
64, 5wa 360 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfwe  4699  wess  4710  weeq1  4711  weeq2  4712  wefr  4713  weso  4714  we0  4718  weinxp  4910  wesn  4914  isowe  6014  isowe2  6015  dfwe2  6358  wexp  6643  wofi  7468  dford5reg  26239
  Copyright terms: Public domain W3C validator