Theorem ssunieq

Description: Relationship implying union. (Contributed by NM, 10-Nov-1999)

	Ref	Expression
Assertion	ssunieq	$$⊢\left(A\in B\wedge \forall x\in Bx\subseteq A\right)\to A=\bigcup B$$

Proof

Step	Hyp	Ref	Expression
1		elssuni	$$⊢A\in B\to A\subseteq \bigcup B$$
2		unissb	$$⊢\bigcup B\subseteq A\leftrightarrow \forall x\in Bx\subseteq A$$
3	2	biimpri	$$⊢\forall x\in Bx\subseteq A\to \bigcup B\subseteq A$$
4	1 3	anim12i	$$⊢\left(A\in B\wedge \forall x\in Bx\subseteq A\right)\to \left(A\subseteq \bigcup B\wedge \bigcup B\subseteq A\right)$$
5		eqss	$$⊢A=\bigcup B\leftrightarrow \left(A\subseteq \bigcup B\wedge \bigcup B\subseteq A\right)$$
6	4 5	sylibr	$$⊢\left(A\in B\wedge \forall x\in Bx\subseteq A\right)\to A=\bigcup B$$