Theorem uniqs2

Description: The union of a quotient set. (Contributed by Mario Carneiro, 11-Jul-2014)

	Ref	Expression
Hypotheses	qsss.1	$$⊢\phi \to R\mathrm{Er}A$$
	qsss.2	$$⊢\phi \to R\in V$$
Assertion	uniqs2	$$⊢\phi \to \bigcup \left(A/R\right)=A$$

Proof

Step	Hyp	Ref	Expression
1		qsss.1	$$⊢\phi \to R\mathrm{Er}A$$
2		qsss.2	$$⊢\phi \to R\in V$$
3		uniqs	$$⊢R\in V\to \bigcup \left(A/R\right)=R\left[A\right]$$
4	2 3	syl	$$⊢\phi \to \bigcup \left(A/R\right)=R\left[A\right]$$
5		erdm	$$⊢R\mathrm{Er}A\to \mathrm{dom}R=A$$
6	1 5	syl	$$⊢\phi \to \mathrm{dom}R=A$$
7	6	imaeq2d	$$⊢\phi \to R\left[\mathrm{dom}R\right]=R\left[A\right]$$
8	4 7	eqtr4d	$$⊢\phi \to \bigcup \left(A/R\right)=R\left[\mathrm{dom}R\right]$$
9		imadmrn	$$⊢R\left[\mathrm{dom}R\right]=\mathrm{ran}R$$
10	8 9	eqtrdi	$$⊢\phi \to \bigcup \left(A/R\right)=\mathrm{ran}R$$
11		errn	$$⊢R\mathrm{Er}A\to \mathrm{ran}R=A$$
12	1 11	syl	$$⊢\phi \to \mathrm{ran}R=A$$
13	10 12	eqtrd	$$⊢\phi \to \bigcup \left(A/R\right)=A$$