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

Metamath Proof Explorer

Theorem iuneq12df

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 31-Dec-2016)

Ref Expression
Hypotheses iuneq12df.1 ⊢ Ⅎ 𝑥 𝜑
iuneq12df.2 ⊢ Ⅎ 𝑥 𝐴
iuneq12df.3 ⊢ Ⅎ 𝑥 𝐵
iuneq12df.4 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
iuneq12df.5 ⊢ ( 𝜑 → 𝐶 = 𝐷 )
Assertion iuneq12df ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 )

Proof

Step Hyp Ref Expression
1 iuneq12df.1 ⊢ Ⅎ 𝑥 𝜑
2 iuneq12df.2 ⊢ Ⅎ 𝑥 𝐴
3 iuneq12df.3 ⊢ Ⅎ 𝑥 𝐵
4 iuneq12df.4 ⊢ ( 𝜑 → 𝐴 = 𝐵 )
5 iuneq12df.5 ⊢ ( 𝜑 → 𝐶 = 𝐷 )
6 5 eleq2d ⊢ ( 𝜑 → ( 𝑦 ∈ 𝐶 ↔ 𝑦 ∈ 𝐷 ) )
7 1 2 3 4 6 rexeqbid ⊢ ( 𝜑 → ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 ) )
8 7 alrimiv ⊢ ( 𝜑 → ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 ) )
9 abbi ⊢ ( ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 ) → { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 } = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 } )
10 df-iun ⊢ ∪ 𝑥 ∈ 𝐴 𝐶 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 }
11 df-iun ⊢ ∪ 𝑥 ∈ 𝐵 𝐷 = { 𝑦 ∣ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 }
12 9 10 11 3eqtr4g ⊢ ( ∀ 𝑦 ( ∃ 𝑥 ∈ 𝐴 𝑦 ∈ 𝐶 ↔ ∃ 𝑥 ∈ 𝐵 𝑦 ∈ 𝐷 ) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 )
13 8 12 syl ⊢ ( 𝜑 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 )