Theorem dfdom2

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

	Ref	Expression
Assertion	dfdom2	⊢ ≼ = ( ≺ ∪ ≈ )

Proof

Step	Hyp	Ref	Expression
1		df-sdom	⊢ ≺ = ( ≼ ∖ ≈ )
2	1	uneq2i	⊢ ( ≈ ∪ ≺ ) = ( ≈ ∪ ( ≼ ∖ ≈ ) )
3		uncom	⊢ ( ≈ ∪ ≺ ) = ( ≺ ∪ ≈ )
4		enssdom	⊢ ≈ ⊆ ≼
5		undif	⊢ ( ≈ ⊆ ≼ ↔ ( ≈ ∪ ( ≼ ∖ ≈ ) ) = ≼ )
6	4 5	mpbi	⊢ ( ≈ ∪ ( ≼ ∖ ≈ ) ) = ≼
7	2 3 6	3eqtr3ri	⊢ ≼ = ( ≺ ∪ ≈ )