Metamath Proof Explorer

Theorem iuneq2

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

Ref Expression
Assertion iuneq2 ⊢∀x∈AB=C→⋃x∈AB=⋃x∈AC

Proof

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