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\leftrightarrow A\cup B=B$$

Proof

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