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

Metamath Proof Explorer

Theorem iuneq12daf

Description: Equality deduction for indexed union, deduction version. (Contributed by Thierry Arnoux, 13-Mar-2017)

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

Proof

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