ssiun3

Description: Subset equivalence for an indexed union. (Contributed by Thierry Arnoux, 17-Oct-2016)

		Ref	Expression
	Assertion	ssiun3	$⊢ \forall y \in C \exists x \in A y \in B \leftrightarrow C \subseteq ⋃_{x \in A} B$

Step	Hyp	Ref	Expression
1		df-ss	$⊢ C \subseteq ⋃_{x \in A} B \leftrightarrow \forall y (y \in C \to y \in ⋃_{x \in A} B)$
2		df-ral	$⊢ \forall y \in C y \in ⋃_{x \in A} B \leftrightarrow \forall y (y \in C \to y \in ⋃_{x \in A} B)$
3		eliun	$⊢ y \in ⋃_{x \in A} B \leftrightarrow \exists x \in A y \in B$
4	3	ralbii	$⊢ \forall y \in C y \in ⋃_{x \in A} B \leftrightarrow \forall y \in C \exists x \in A y \in B$
5	1 2 4	3bitr2ri	$⊢ \forall y \in C \exists x \in A y \in B \leftrightarrow C \subseteq ⋃_{x \in A} B$

Metamath Proof Explorer