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

Definition df-sdom 7272
Description: Define the strict dominance relation. Alternate possible definitions are derived as brsdom 7291 and brsdom2 7394. Definition 3 of [Suppes] p. 97. (Contributed by NM, 31-Mar-1998.)
Assertion
Ref Expression
df-sdom

Detailed syntax breakdown of Definition df-sdom
StepHypRef Expression
1 csdm 7268 . 2
2 cdom 7267 . . 3
3 cen 7266 . . 3
42, 3cdif 3302 . 2
51, 4wceq 1687 1
Colors of variables: wff setvar class
This definition is referenced by:  relsdom  7276  brsdom  7291  dfdom2  7294  dfsdom2  7393
  Copyright terms: Public domain W3C validator