This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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	$⊢ ≺ = ≼ ∖ ≼^{-1}$

Step	Hyp	Ref	Expression
1		df-sdom	$⊢ ≺ = ≼ ∖ \approx$
2		sbthcl	$⊢ \approx = ≼ \cap ≼^{-1}$
3	2	difeq2i	$⊢ ≼ ∖ \approx = ≼ ∖ (≼ \cap ≼^{-1})$
4		difin	$⊢ ≼ ∖ (≼ \cap ≼^{-1}) = ≼ ∖ ≼^{-1}$
5	1 3 4	3eqtri	$⊢ ≺ = ≼ ∖ ≼^{-1}$