Theorem rncossdmcoss

Description: The range of cosets is the domain of them (this should be rncoss but there exists a theorem with this name already). (Contributed by Peter Mazsa, 12-Dec-2019)

	Ref	Expression
Assertion	rncossdmcoss	$$⊢\mathrm{ran}\wr R=\mathrm{dom}\wr R$$

Proof

Step	Hyp	Ref	Expression
1		brcosscnvcoss	$$⊢\left(y\in \mathrm{V}\wedge x\in \mathrm{V}\right)\to \left(y\wr Rx\leftrightarrow x\wr Ry\right)$$
2	1	el2v	$$⊢y\wr Rx\leftrightarrow x\wr Ry$$
3	2	exbii	$$⊢\exists yy\wr Rx\leftrightarrow \exists yx\wr Ry$$
4	3	abbii	$$⊢\left\{x|\exists yy\wr Rx\right\}=\left\{x|\exists yx\wr Ry\right\}$$
5		dfrn2	$$⊢\mathrm{ran}\wr R=\left\{x|\exists yy\wr Rx\right\}$$
6		df-dm	$$⊢\mathrm{dom}\wr R=\left\{x|\exists yx\wr Ry\right\}$$
7	4 5 6	3eqtr4i	$$⊢\mathrm{ran}\wr R=\mathrm{dom}\wr R$$