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

Metamath Proof Explorer

Theorem dfdom2

Description: Alternate definition of dominance. (Contributed by NM, 17-Jun-1998)

		Ref	Expression
	Assertion	dfdom2	$⊢ ≼ = ≺ \cup \approx$

Step	Hyp	Ref	Expression
1		df-sdom	$⊢ ≺ = ≼ ∖ \approx$
2	1	uneq2i	$⊢ \approx \cup ≺ = \approx \cup (≼ ∖ \approx)$
3		uncom	$⊢ \approx \cup ≺ = ≺ \cup \approx$
4		enssdom	$⊢ \approx \subseteq ≼$
5		undif	$⊢ \approx \subseteq ≼ \leftrightarrow \approx \cup (≼ ∖ \approx) = ≼$
6	4 5	mpbi	$⊢ \approx \cup (≼ ∖ \approx) = ≼$
7	2 3 6	3eqtr3ri	$⊢ ≼ = ≺ \cup \approx$