Metamath Proof Explorer


Definition df-sdom

Description: Define the strict dominance relation. Alternate possible definitions are derived as brsdom and brsdom2 . Definition 3 of Suppes p. 97. (Contributed by NM, 31-Mar-1998)

Ref Expression
Assertion df-sdom =

Detailed syntax breakdown

Step Hyp Ref Expression
0 csdm class
1 cdom class
2 cen class
3 1 2 cdif class
4 0 3 wceq wff =