This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem uniqs2

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

Ref Expression
Hypotheses qsss.1 ⊢ φ → R Er A
qsss.2 ⊢ φ → R ∈ V
Assertion uniqs2 ⊢ φ → ⋃ A / R = A

Proof

Step Hyp Ref Expression
1 qsss.1 ⊢ φ → R Er A
2 qsss.2 ⊢ φ → R ∈ V
3 uniqsw ⊢ R ∈ V → ⋃ A / R = R A
4 2 3 syl ⊢ φ → ⋃ A / R = R A
5 erdm ⊢ R Er A → dom ⁡ R = A
6 1 5 syl ⊢ φ → dom ⁡ R = A
7 6 imaeq2d ⊢ φ → R dom ⁡ R = R A
8 4 7 eqtr4d ⊢ φ → ⋃ A / R = R dom ⁡ R
9 imadmrn ⊢ R dom ⁡ R = ran ⁡ R
10 8 9 eqtrdi ⊢ φ → ⋃ A / R = ran ⁡ R
11 errn ⊢ R Er A → ran ⁡ R = A
12 1 11 syl ⊢ φ → ran ⁡ R = A
13 10 12 eqtrd ⊢ φ → ⋃ A / R = A