Definition df-sdom 6820

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

Assertion

Ref	Expression
df-sdom	|- ~< = ( ~<_ \ ~~ )

Detailed syntax breakdown of Definition df-sdom

Step	Hyp	Ref	Expression
1		csdm 6816	. 2 class ~<
2		cdom 6815	. . 3 class ~<_
3		cen 6814	. . 3 class ~~
4	2, 3	cdif 3110	. 2 class ( ~<_ \ ~~ )
5	1, 4	wceq 1619	1 wff ~< = ( ~<_ \ ~~ )

This definition is referenced by:  relsdom  6824  brsdom  6838  dfdom2  6841  dfsdom2  6938