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

Definition df-we 4584
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 4803. (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 4581 . 2
41, 2wfr 4579 . . 3
51, 2wor 4543 . . 3
64, 5wa 360 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfwe  4599  wess  4610  weeq1  4611  weeq2  4612  wefr  4613  weso  4614  we0  4618  dfwe2  4803  weinxp  4985  wesn  4989  isowe  6117  isowe2  6118  wexp  6510  wofi  7405  dford5reg  25513
  Copyright terms: Public domain W3C validator