Theorem dfsdom2

Description: Alternate definition of strict dominance. Compare Definition 3 of Suppes p. 97. (Contributed by NM, 31-Mar-1998)

	Ref	Expression
Assertion	dfsdom2	⊢ ≺ = ( ≼ ∖ ◡ ≼ )

Proof

Step	Hyp	Ref	Expression
1		df-sdom	⊢ ≺ = ( ≼ ∖ ≈ )
2		sbthcl	⊢ ≈ = ( ≼ ∩ ◡ ≼ )
3	2	difeq2i	⊢ ( ≼ ∖ ≈ ) = ( ≼ ∖ ( ≼ ∩ ◡ ≼ ) )
4		difin	⊢ ( ≼ ∖ ( ≼ ∩ ◡ ≼ ) ) = ( ≼ ∖ ◡ ≼ )
5	1 3 4	3eqtri	⊢ ≺ = ( ≼ ∖ ◡ ≼ )