Definition df-sdom 3276

Description: Define strict dominance relation. Alternate possible definitions are derived as brsdom 3286 and brsdom2 3363. Definition 3 of [Suppes] p. 97.

Assertion

Ref	Expression
df-sdom	⊢ ≺ = ( ≼ ∖ ≈ )

Detailed syntax breakdown of Definition df-sdom

Step	Hyp	Ref	Expression
1		csdm 3273	. 2 class ≺
2		cdom 3272	. . 3 class ≼
3		cen 3271	. . 3 class ≈
4	2, 3	cdif 1484	. 2 class ( ≼ ∖ ≈ )
5	1, 4	wceq 1091	1 wff ≺ = ( ≼ ∖ ≈ )

This definition is referenced by:  relsdom 3279  brsdom 3286  dfdom2 3288  dfsdom2 3362

metamath.org