Theorem uniqs

Description: The union of a quotient set, like uniqsw but with a weaker antecedent: only the restriction of R by A needs to be a set, not R itself, see e.g. cnvepima . (Contributed by NM, 9-Dec-2008) (Revised by Peter Mazsa, 20-Jun-2019)

	Ref	Expression
Assertion	uniqs	$$⊢{R\upharpoonright }_A\in V\to \bigcup \left(A/R\right)=R\left[A\right]$$

Proof

Step	Hyp	Ref	Expression
1		elecex	$$⊢{R\upharpoonright }_A\in V\to \left(x\in A\to \left[x\right]R\in \mathrm{V}\right)$$
2	1	ralrimiv	$$⊢{R\upharpoonright }_A\in V\to \forall x\in A\left[x\right]R\in \mathrm{V}$$
3		dfiun2g	$$⊢\forall x\in A\left[x\right]R\in \mathrm{V}\to \bigcup _{x\in A}\left[x\right]R=\bigcup \left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
4	2 3	syl	$$⊢{R\upharpoonright }_A\in V\to \bigcup _{x\in A}\left[x\right]R=\bigcup \left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
5	4	eqcomd	$$⊢{R\upharpoonright }_A\in V\to \bigcup \left\{y|\exists x\in Ay=\left[x\right]R\right\}=\bigcup _{x\in A}\left[x\right]R$$
6		df-qs	$$⊢A/R=\left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
7	6	unieqi	$$⊢\bigcup \left(A/R\right)=\bigcup \left\{y|\exists x\in Ay=\left[x\right]R\right\}$$
8		df-ec	$$⊢\left[x\right]R=R\left[\left\{x\right\}\right]$$
9	8	a1i	$$⊢x\in A\to \left[x\right]R=R\left[\left\{x\right\}\right]$$
10	9	iuneq2i	$$⊢\bigcup _{x\in A}\left[x\right]R=\bigcup _{x\in A}R\left[\left\{x\right\}\right]$$
11		imaiun	$$⊢R\left[\bigcup _{x\in A}\left\{x\right\}\right]=\bigcup _{x\in A}R\left[\left\{x\right\}\right]$$
12		iunid	$$⊢\bigcup _{x\in A}\left\{x\right\}=A$$
13	12	imaeq2i	$$⊢R\left[\bigcup _{x\in A}\left\{x\right\}\right]=R\left[A\right]$$
14	10 11 13	3eqtr2ri	$$⊢R\left[A\right]=\bigcup _{x\in A}\left[x\right]R$$
15	5 7 14	3eqtr4g	$$⊢{R\upharpoonright }_A\in V\to \bigcup \left(A/R\right)=R\left[A\right]$$