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

Definition df-we 4652
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6363. (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 4649 . 2
41, 2wfr 4647 . . 3
51, 2wor 4611 . . 3
64, 5wa 362 . 2
73, 6wb 178 1
Colors of variables: wff setvar class
This definition is referenced by:  nfwe  4667  wess  4678  weeq1  4679  weeq2  4680  wefr  4681  weso  4682  we0  4686  weinxp  4877  wesn  4881  isowe  6008  isowe2  6009  dfwe2  6363  wexp  6655  wofi  7520  dford5reg  27297  fin2so  28087
  Copyright terms: Public domain W3C validator