Definition df-sdom 8976

Description: Define the strict dominance relation. Alternate possible definitions are derived as brsdom 9001 and brsdom2 9120. 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 8972	. 2 class ≺
2		cdom 8971	. . 3 class ≼
3		cen 8970	. . 3 class ≈
4	2, 3	cdif 4045	. 2 class ( ≼ ∖ ≈ )
5	1, 4	wceq 1569	1 wff ≺ = ( ≼ ∖ ≈ )

This definition is used by:  relsdom  8980  brsdom  9001  dfdom2  9005  dfsdom2  9119