ssunieq

		Ref	Expression
	Assertion	ssunieq	$⊢ (A \in B \land \forall x \in B x \subseteq A) \to A = ⋃ B$

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

Metamath Proof Explorer