# Metamath Proof Explorer

## Theorem iunss

Description: Subset theorem for an indexed union. (Contributed by NM, 13-Sep-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iunss ${⊢}\bigcup _{{x}\in {A}}{B}\subseteq {C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}$

### Proof

Step Hyp Ref Expression
1 df-iun ${⊢}\bigcup _{{x}\in {A}}{B}=\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\right\}$
2 1 sseq1i ${⊢}\bigcup _{{x}\in {A}}{B}\subseteq {C}↔\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\right\}\subseteq {C}$
3 abss ${⊢}\left\{{y}|\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\right\}\subseteq {C}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to {y}\in {C}\right)$
4 dfss2 ${⊢}{B}\subseteq {C}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {y}\in {C}\right)$
5 4 ralbii ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {y}\in {C}\right)$
6 ralcom4 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {y}\in {C}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {y}\in {C}\right)$
7 r19.23v ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {y}\in {C}\right)↔\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to {y}\in {C}\right)$
8 7 albii ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}\left({y}\in {B}\to {y}\in {C}\right)↔\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to {y}\in {C}\right)$
9 5 6 8 3bitrri ${⊢}\forall {y}\phantom{\rule{.4em}{0ex}}\left(\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}\to {y}\in {C}\right)↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}$
10 2 3 9 3bitri ${⊢}\bigcup _{{x}\in {A}}{B}\subseteq {C}↔\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\subseteq {C}$