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

Metamath Proof Explorer

Theorem relsdom

Description: Strict dominance is a relation. (Contributed by NM, 31-Mar-1998)

		Ref	Expression
	Assertion	relsdom	$⊢ Rel ≺$

Step	Hyp	Ref	Expression
1		reldom	$⊢ Rel ≼$
2		reldif	$⊢ Rel ≼ \to Rel (≼ ∖ \approx)$
3		df-sdom	$⊢ ≺ = ≼ ∖ \approx$
4	3	releqi	$⊢ Rel ≺ \leftrightarrow Rel (≼ ∖ \approx)$
5	2 4	sylibr	$⊢ Rel ≼ \to Rel ≺$
6	1 5	ax-mp	$⊢ Rel ≺$