# Metamath Proof Explorer

## Theorem ssuni

Description: Subclass relationship for class union. (Contributed by NM, 24-May-1994) (Proof shortened by Andrew Salmon, 29-Jun-2011) (Proof shortened by JJ, 26-Jul-2021)

Ref Expression
Assertion ssuni ${⊢}\left({A}\subseteq {B}\wedge {B}\in {C}\right)\to {A}\subseteq \bigcup {C}$

### Proof

Step Hyp Ref Expression
1 elunii ${⊢}\left({x}\in {B}\wedge {B}\in {C}\right)\to {x}\in \bigcup {C}$
2 1 expcom ${⊢}{B}\in {C}\to \left({x}\in {B}\to {x}\in \bigcup {C}\right)$
3 2 imim2d ${⊢}{B}\in {C}\to \left(\left({x}\in {A}\to {x}\in {B}\right)\to \left({x}\in {A}\to {x}\in \bigcup {C}\right)\right)$
4 3 alimdv ${⊢}{B}\in {C}\to \left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)\to \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in \bigcup {C}\right)\right)$
5 dfss2 ${⊢}{A}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)$
6 dfss2 ${⊢}{A}\subseteq \bigcup {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in \bigcup {C}\right)$
7 4 5 6 3imtr4g ${⊢}{B}\in {C}\to \left({A}\subseteq {B}\to {A}\subseteq \bigcup {C}\right)$
8 7 impcom ${⊢}\left({A}\subseteq {B}\wedge {B}\in {C}\right)\to {A}\subseteq \bigcup {C}$