# Metamath Proof Explorer

## Theorem iuneq2

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

Ref Expression
Assertion iuneq2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \bigcup _{{x}\in {A}}{B}=\bigcup _{{x}\in {A}}{C}$

### Proof

Step Hyp Ref Expression
1 ss2iun ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\to \bigcup _{{x}\in {A}}{B}\subseteq \bigcup _{{x}\in {A}}{C}$
2 ss2iun ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\to \bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{x}\in {A}}{B}$
3 1 2 anim12i ${⊢}\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)\to \left(\bigcup _{{x}\in {A}}{B}\subseteq \bigcup _{{x}\in {A}}{C}\wedge \bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{x}\in {A}}{B}\right)$
4 eqss ${⊢}{B}={C}↔\left({B}\subseteq {C}\wedge {C}\subseteq {B}\right)$
5 4 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {C}\wedge {C}\subseteq {B}\right)$
6 r19.26 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({B}\subseteq {C}\wedge {C}\subseteq {B}\right)↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)$
7 5 6 bitri ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}↔\left(\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{C}\subseteq {B}\right)$
8 eqss ${⊢}\bigcup _{{x}\in {A}}{B}=\bigcup _{{x}\in {A}}{C}↔\left(\bigcup _{{x}\in {A}}{B}\subseteq \bigcup _{{x}\in {A}}{C}\wedge \bigcup _{{x}\in {A}}{C}\subseteq \bigcup _{{x}\in {A}}{B}\right)$
9 3 7 8 3imtr4i ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}={C}\to \bigcup _{{x}\in {A}}{B}=\bigcup _{{x}\in {A}}{C}$