# Metamath Proof Explorer

## Theorem iuneq1

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

Ref Expression
Assertion iuneq1 ${⊢}{A}={B}\to \bigcup _{{x}\in {A}}{C}=\bigcup _{{x}\in {B}}{C}$

### Proof

Step Hyp Ref Expression
1 iunss1 ${⊢}{A}\subseteq {B}\to \bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{x}\in {B}}{C}$
2 iunss1 ${⊢}{B}\subseteq {A}\to \bigcup _{{x}\in {B}}{C}\subseteq \bigcup _{{x}\in {A}}{C}$
3 1 2 anim12i ${⊢}\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)\to \left(\bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{x}\in {B}}{C}\wedge \bigcup _{{x}\in {B}}{C}\subseteq \bigcup _{{x}\in {A}}{C}\right)$
4 eqss ${⊢}{A}={B}↔\left({A}\subseteq {B}\wedge {B}\subseteq {A}\right)$
5 eqss ${⊢}\bigcup _{{x}\in {A}}{C}=\bigcup _{{x}\in {B}}{C}↔\left(\bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{x}\in {B}}{C}\wedge \bigcup _{{x}\in {B}}{C}\subseteq \bigcup _{{x}\in {A}}{C}\right)$
6 3 4 5 3imtr4i ${⊢}{A}={B}\to \bigcup _{{x}\in {A}}{C}=\bigcup _{{x}\in {B}}{C}$