Theorem uniqs2

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

	Ref	Expression
Hypotheses	qsss.1	⊢ ( 𝜑 → 𝑅 Er 𝐴 )
	qsss.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
Assertion	uniqs2	⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = 𝐴 )

Proof

Step	Hyp	Ref	Expression
1		qsss.1	⊢ ( 𝜑 → 𝑅 Er 𝐴 )
2		qsss.2	⊢ ( 𝜑 → 𝑅 ∈ 𝑉 )
3		uniqsw	⊢ ( 𝑅 ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )
4	2 3	syl	⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )
5		erdm	⊢ ( 𝑅 Er 𝐴 → dom 𝑅 = 𝐴 )
6	1 5	syl	⊢ ( 𝜑 → dom 𝑅 = 𝐴 )
7	6	imaeq2d	⊢ ( 𝜑 → ( 𝑅 “ dom 𝑅 ) = ( 𝑅 “ 𝐴 ) )
8	4 7	eqtr4d	⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ dom 𝑅 ) )
9		imadmrn	⊢ ( 𝑅 “ dom 𝑅 ) = ran 𝑅
10	8 9	eqtrdi	⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = ran 𝑅 )
11		errn	⊢ ( 𝑅 Er 𝐴 → ran 𝑅 = 𝐴 )
12	1 11	syl	⊢ ( 𝜑 → ran 𝑅 = 𝐴 )
13	10 12	eqtrd	⊢ ( 𝜑 → ∪ ( 𝐴 / 𝑅 ) = 𝐴 )