Theorem dfdom2

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

	Ref	Expression
Assertion	dfdom2	$$⊢\preccurlyeq =\prec \cup \approx$$

Proof

Step	Hyp	Ref	Expression
1		df-sdom	$$⊢\prec =\preccurlyeq \setminus \approx$$
2	1	uneq2i	$$⊢\approx \cup \prec =\approx \cup \left(\preccurlyeq \setminus \approx \right)$$
3		uncom	$$⊢\approx \cup \prec =\prec \cup \approx$$
4		enssdom	$$⊢\approx \subseteq \preccurlyeq$$
5		undif	$$⊢\approx \subseteq \preccurlyeq \leftrightarrow \approx \cup \left(\preccurlyeq \setminus \approx \right)=\preccurlyeq$$
6	4 5	mpbi	$$⊢\approx \cup \left(\preccurlyeq \setminus \approx \right)=\preccurlyeq$$
7	2 3 6	3eqtr3ri	$$⊢\preccurlyeq =\prec \cup \approx$$