# Metamath Proof Explorer

## Theorem ssequn1

Description: A relationship between subclass and union. Theorem 26 of Suppes p. 27. (Contributed by NM, 30-Aug-1993) (Proof shortened by Andrew Salmon, 26-Jun-2011)

Ref Expression
Assertion ssequn1 ${⊢}{A}\subseteq {B}↔{A}\cup {B}={B}$

### Proof

Step Hyp Ref Expression
1 bicom ${⊢}\left({x}\in {B}↔\left({x}\in {A}\vee {x}\in {B}\right)\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)↔{x}\in {B}\right)$
2 pm4.72 ${⊢}\left({x}\in {A}\to {x}\in {B}\right)↔\left({x}\in {B}↔\left({x}\in {A}\vee {x}\in {B}\right)\right)$
3 elun ${⊢}{x}\in \left({A}\cup {B}\right)↔\left({x}\in {A}\vee {x}\in {B}\right)$
4 3 bibi1i ${⊢}\left({x}\in \left({A}\cup {B}\right)↔{x}\in {B}\right)↔\left(\left({x}\in {A}\vee {x}\in {B}\right)↔{x}\in {B}\right)$
5 1 2 4 3bitr4i ${⊢}\left({x}\in {A}\to {x}\in {B}\right)↔\left({x}\in \left({A}\cup {B}\right)↔{x}\in {B}\right)$
6 5 albii ${⊢}\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup {B}\right)↔{x}\in {B}\right)$
7 dfss2 ${⊢}{A}\subseteq {B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in {A}\to {x}\in {B}\right)$
8 dfcleq ${⊢}{A}\cup {B}={B}↔\forall {x}\phantom{\rule{.4em}{0ex}}\left({x}\in \left({A}\cup {B}\right)↔{x}\in {B}\right)$
9 6 7 8 3bitr4i ${⊢}{A}\subseteq {B}↔{A}\cup {B}={B}$