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	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )

Proof

Step	Hyp	Ref	Expression
1		elecex	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ( 𝑥 ∈ 𝐴 → [ 𝑥 ] 𝑅 ∈ V ) )
2	1	ralrimiv	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∀ 𝑥 ∈ 𝐴 [ 𝑥 ] 𝑅 ∈ 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	⊢ ( ( 𝑅 ↾ 𝐴 ) ∈ 𝑉 → ∪ ( 𝐴 / 𝑅 ) = ( 𝑅 “ 𝐴 ) )