Theorem uniqs2

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

	Ref	Expression
Hypotheses	qsss.1	|- ( ph -> R Er A )
	qsss.2	|- ( ph -> R e. V )
Assertion	uniqs2	|- ( ph -> U. ( A /. R ) = A )

Proof

Step	Hyp	Ref	Expression
1		qsss.1	|- ( ph -> R Er A )
2		qsss.2	|- ( ph -> R e. V )
3		uniqs	|- ( R e. V -> U. ( A /. R ) = ( R " A ) )
4	2 3	syl	|- ( ph -> U. ( A /. R ) = ( R " A ) )
5		erdm	|- ( R Er A -> dom R = A )
6	1 5	syl	|- ( ph -> dom R = A )
7	6	imaeq2d	|- ( ph -> ( R " dom R ) = ( R " A ) )
8	4 7	eqtr4d	|- ( ph -> U. ( A /. R ) = ( R " dom R ) )
9		imadmrn	|- ( R " dom R ) = ran R
10	8 9	eqtrdi	|- ( ph -> U. ( A /. R ) = ran R )
11		errn	|- ( R Er A -> ran R = A )
12	1 11	syl	|- ( ph -> ran R = A )
13	10 12	eqtrd	|- ( ph -> U. ( A /. R ) = A )