# Metamath Proof Explorer

## Theorem ssiun3

Description: Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016)

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

### Proof

Step Hyp Ref Expression
1 dfss2 ${⊢}{C}\subseteq \bigcup _{{x}\in {A}}{B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\to {y}\in \bigcup _{{x}\in {A}}{B}\right)$
2 df-ral ${⊢}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{y}\in \bigcup _{{x}\in {A}}{B}↔\forall {y}\phantom{\rule{.4em}{0ex}}\left({y}\in {C}\to {y}\in \bigcup _{{x}\in {A}}{B}\right)$
3 eliun ${⊢}{y}\in \bigcup _{{x}\in {A}}{B}↔\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
4 3 ralbii ${⊢}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}{y}\in \bigcup _{{x}\in {A}}{B}↔\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}$
5 1 2 4 3bitr2ri ${⊢}\forall {y}\in {C}\phantom{\rule{.4em}{0ex}}\exists {x}\in {A}\phantom{\rule{.4em}{0ex}}{y}\in {B}↔{C}\subseteq \bigcup _{{x}\in {A}}{B}$