Theorem uniqs

Description: The union of a quotient set. (Contributed by NM, 9-Dec-2008)

	Ref	Expression
Assertion	uniqs	⊢ ( 𝑅 ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		ecexg	⊢ ( 𝑅 ∈ 𝑉 → [ 𝑥 ] 𝑅 ∈ V )
2	1	ralrimivw	⊢ ( 𝑅 ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ∈ V )
3		dfiun2g	⊢ ( ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ∈ V → ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } )
4	2 3	syl	⊢ ( 𝑅 ∈ 𝑉 → ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } )
5	4	eqcomd	⊢ ( 𝑅 ∈ 𝑉 → ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 } = ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 )
6		df-qs	⊢ ( 𝐴 / 𝑅 ) = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
7	6	unieqi	⊢ ∪ ( 𝐴 / 𝑅 ) = ∪ { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 = [ 𝑥 ] 𝑅 }
8		df-ec	⊢ [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } )
9	8	a1i	⊢ ( 𝑥 ∈ 𝐴 → [ 𝑥 ] 𝑅 = ( 𝑅 “ { 𝑥 } ) )
10	9	iuneq2i	⊢ ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 = ∪ 𝑥 ∈ 𝐴 ( 𝑅 “ { 𝑥 } )
11		imaiun	⊢ ( 𝑅 “ ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) = ∪ 𝑥 ∈ 𝐴 ( 𝑅 “ { 𝑥 } )
12		iunid	⊢ ∪ 𝑥 ∈ 𝐴 { 𝑥 } = 𝐴
13	12	imaeq2i	⊢ ( 𝑅 “ ∪ 𝑥 ∈ 𝐴 { 𝑥 } ) = ( 𝑅 “ 𝐴 )
14	10 11 13	3eqtr2ri	⊢ ( 𝑅 “ 𝐴 ) = ∪ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅
15	5 7 14	3eqtr4g	⊢ ( 𝑅 ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )