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

Definition df-we 4702
Description: Define the well-ordering predicate. For an alternate definition, see dfwe2 6403. (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 4699 . 2
41, 2wfr 4697 . . 3
51, 2wor 4661 . . 3
64, 5wa 360 . 2
73, 6wb 178 1
Colors of variables: wff set class
This definition is referenced by:  nfwe  4717  wess  4728  weeq1  4729  weeq2  4730  wefr  4731  weso  4732  we0  4736  weinxp  4928  wesn  4932  isowe  6050  isowe2  6051  dfwe2  6403  wexp  6692  wofi  7522  dford5reg  26748
  Copyright terms: Public domain W3C validator