Metamath Proof Explorer

Theorem iuneq2

Description: Equality theorem for indexed union. (Contributed by NM, 22-Oct-2003)

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

Proof

Step Hyp Ref Expression
1 ss2iun ⊢ ∀ x ∈ A B ⊆ C → ⋃ x ∈ A B ⊆ ⋃ x ∈ A C
2 ss2iun ⊢ ∀ x ∈ A C ⊆ B → ⋃ x ∈ A C ⊆ ⋃ x ∈ A B
3 1 2 anim12i ⊢ ∀ x ∈ A B ⊆ C ∧ ∀ x ∈ A C ⊆ B → ⋃ x ∈ A B ⊆ ⋃ x ∈ A C ∧ ⋃ x ∈ A C ⊆ ⋃ x ∈ A B
4 eqss ⊢ B = C ↔ B ⊆ C ∧ C ⊆ B
5 4 ralbii ⊢ ∀ x ∈ A B = C ↔ ∀ x ∈ A B ⊆ C ∧ C ⊆ B
6 r19.26 ⊢ ∀ x ∈ A B ⊆ C ∧ C ⊆ B ↔ ∀ x ∈ A B ⊆ C ∧ ∀ x ∈ A C ⊆ B
7 5 6 bitri ⊢ ∀ x ∈ A B = C ↔ ∀ x ∈ A B ⊆ C ∧ ∀ x ∈ A C ⊆ B
8 eqss ⊢ ⋃ x ∈ A B = ⋃ x ∈ A C ↔ ⋃ x ∈ A B ⊆ ⋃ x ∈ A C ∧ ⋃ x ∈ A C ⊆ ⋃ x ∈ A B
9 3 7 8 3imtr4i ⊢ ∀ x ∈ A B = C → ⋃ x ∈ A B = ⋃ x ∈ A C