Theorem dfrn6

Description: Alternate definition of range. (Contributed by Peter Mazsa, 1-Aug-2018)

	Ref	Expression
Assertion	dfrn6	$$⊢\mathrm{ran}R=\left\{x|\left[x\right]R^{-1}\ne \varnothing \right\}$$

Proof

Step	Hyp	Ref	Expression
1		df-rn	$$⊢\mathrm{ran}R=\mathrm{dom}{R}^{-1}$$
2		dfdm6	$$⊢\mathrm{dom}{R}^{-1}=\left\{x|\left[x\right]R^{-1}\ne \varnothing \right\}$$
3	1 2	eqtri	$$⊢\mathrm{ran}R=\left\{x|\left[x\right]R^{-1}\ne \varnothing \right\}$$