Description: Equality deduction for indexed unions. (Contributed by Giovanni Mascellani, 10-Apr-2018)
Ref | Expression | ||
---|---|---|---|
Hypotheses | iuneq12f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
iuneq12f.2 | ⊢ Ⅎ 𝑥 𝐵 | ||
Assertion | iuneq12f | ⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 ) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | iuneq12f.1 | ⊢ Ⅎ 𝑥 𝐴 | |
2 | iuneq12f.2 | ⊢ Ⅎ 𝑥 𝐵 | |
3 | iuneq2 | ⊢ ( ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐴 𝐷 ) | |
4 | 1 2 | iuneq2f | ⊢ ( 𝐴 = 𝐵 → ∪ 𝑥 ∈ 𝐴 𝐷 = ∪ 𝑥 ∈ 𝐵 𝐷 ) |
5 | 3 4 | sylan9eqr | ⊢ ( ( 𝐴 = 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 𝐶 = 𝐷 ) → ∪ 𝑥 ∈ 𝐴 𝐶 = ∪ 𝑥 ∈ 𝐵 𝐷 ) |