# Metamath Proof Explorer

## Theorem unss

Description: The union of two subclasses is a subclass. Theorem 27 of Suppes p. 27 and its converse. (Contributed by NM, 11-Jun-2004)

Ref Expression
Assertion unss ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}\cup {B}\subseteq {C}$

### Proof

Step Hyp Ref Expression
1 dfss2 ${⊢}{A}\cup {B}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup {B}\right)\to {x}\in {C}\right)$
2 19.26 ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {x}\in {C}\right)\wedge \left({x}\in {B}\to {x}\in {C}\right)\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {C}\right)\right)$
3 elunant ${⊢}\left({x}\in \left({A}\cup {B}\right)\to {x}\in {C}\right)↔\left(\left({x}\in {A}\to {x}\in {C}\right)\wedge \left({x}\in {B}\to {x}\in {C}\right)\right)$
4 3 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup {B}\right)\to {x}\in {C}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left(\left({x}\in {A}\to {x}\in {C}\right)\wedge \left({x}\in {B}\to {x}\in {C}\right)\right)$
5 dfss2 ${⊢}{A}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)$
6 dfss2 ${⊢}{B}\subseteq {C}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {C}\right)$
7 5 6 anbi12i ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔\left(\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {C}\right)\wedge \forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {B}\to {x}\in {C}\right)\right)$
8 2 4 7 3bitr4i ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup {B}\right)\to {x}\in {C}\right)↔\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)$
9 1 8 bitr2i ${⊢}\left({A}\subseteq {C}\wedge {B}\subseteq {C}\right)↔{A}\cup {B}\subseteq {C}$