# Metamath Proof Explorer

## Theorem uniss

Description: Subclass relationship for class union. Theorem 61 of Suppes p. 39. (Contributed by NM, 22-Mar-1998) (Proof shortened by Andrew Salmon, 29-Jun-2011)

Ref Expression
Assertion uniss ${⊢}{A}\subseteq {B}\to \bigcup {A}\subseteq \bigcup {B}$

### Proof

Step Hyp Ref Expression
1 ssel ${⊢}{A}\subseteq {B}\to \left({y}\in {A}\to {y}\in {B}\right)$
2 1 anim2d ${⊢}{A}\subseteq {B}\to \left(\left({x}\in {y}\wedge {y}\in {A}\right)\to \left({x}\in {y}\wedge {y}\in {B}\right)\right)$
3 2 eximdv ${⊢}{A}\subseteq {B}\to \left(\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {A}\right)\to \exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {B}\right)\right)$
4 eluni ${⊢}{x}\in \bigcup {A}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {A}\right)$
5 eluni ${⊢}{x}\in \bigcup {B}↔\exists {y}\phantom{\rule{.4em}{0ex}}\left({x}\in {y}\wedge {y}\in {B}\right)$
6 3 4 5 3imtr4g ${⊢}{A}\subseteq {B}\to \left({x}\in \bigcup {A}\to {x}\in \bigcup {B}\right)$
7 6 ssrdv ${⊢}{A}\subseteq {B}\to \bigcup {A}\subseteq \bigcup {B}$