Metamath Proof Explorer

Theorem iuneq1

Description: Equality theorem for indexed union. (Contributed by NM, 27-Jun-1998)

Ref Expression
Assertion iuneq1 ⊢ A = B → ⋃ x ∈ A C = ⋃ x ∈ B C

Proof

Step Hyp Ref Expression
1 iunss1 ⊢ A ⊆ B → ⋃ x ∈ A C ⊆ ⋃ x ∈ B C
2 iunss1 ⊢ B ⊆ A → ⋃ x ∈ B C ⊆ ⋃ x ∈ A C
3 1 2 anim12i ⊢ A ⊆ B ∧ B ⊆ A → ⋃ x ∈ A C ⊆ ⋃ x ∈ B C ∧ ⋃ x ∈ B C ⊆ ⋃ x ∈ A C
4 eqss ⊢ A = B ↔ A ⊆ B ∧ B ⊆ A
5 eqss ⊢ ⋃ x ∈ A C = ⋃ x ∈ B C ↔ ⋃ x ∈ A C ⊆ ⋃ x ∈ B C ∧ ⋃ x ∈ B C ⊆ ⋃ x ∈ A C
6 3 4 5 3imtr4i ⊢ A = B → ⋃ x ∈ A C = ⋃ x ∈ B C