Theorem unidif

Description: If the difference A \ B contains the largest members of A , then the union of the difference is the union of A . (Contributed by NM, 22-Mar-2004)

	Ref	Expression
Assertion	unidif	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)x\subseteq y\to \bigcup \left(A\setminus B\right)=\bigcup A$$

Proof

Step	Hyp	Ref	Expression
1		uniss2	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)x\subseteq y\to \bigcup A\subseteq \bigcup \left(A\setminus B\right)$$
2		difss	$$⊢A\setminus B\subseteq A$$
3	2	unissi	$$⊢\bigcup \left(A\setminus B\right)\subseteq \bigcup A$$
4	1 3	jctil	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)x\subseteq y\to \left(\bigcup \left(A\setminus B\right)\subseteq \bigcup A\wedge \bigcup A\subseteq \bigcup \left(A\setminus B\right)\right)$$
5		eqss	$$⊢\bigcup \left(A\setminus B\right)=\bigcup A\leftrightarrow \left(\bigcup \left(A\setminus B\right)\subseteq \bigcup A\wedge \bigcup A\subseteq \bigcup \left(A\setminus B\right)\right)$$
6	4 5	sylibr	$$⊢\forall x\in A\exists y\in \left(A\setminus B\right)x\subseteq y\to \bigcup \left(A\setminus B\right)=\bigcup A$$