Theorem dfdm6

Description: Alternate definition of domain. (Contributed by Peter Mazsa, 2-Mar-2018)

	Ref	Expression
Assertion	dfdm6	$$⊢\mathrm{dom}R=\left\{x|\left[x\right]R\ne \varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		ecdmn0	$$⊢x\in \mathrm{dom}R\leftrightarrow \left[x\right]R\ne \varnothing$$
2	1	eqabi	$$⊢\mathrm{dom}R=\left\{x|\left[x\right]R\ne \varnothing \right\}$$