elunii

		Ref	Expression
	Assertion	elunii	$⊢ (A \in B \land B \in C) \to A \in ⋃ C$

Step	Hyp	Ref	Expression
1		eleq2	$⊢ x = B \to (A \in x \leftrightarrow A \in B)$
2		eleq1	$⊢ x = B \to (x \in C \leftrightarrow B \in C)$
3	1 2	anbi12d	$⊢ x = B \to ((A \in x \land x \in C) \leftrightarrow (A \in B \land B \in C))$
4	3	spcegv	$⊢ B \in C \to ((A \in B \land B \in C) \to \exists x (A \in x \land x \in C))$
5	4	anabsi7	$⊢ (A \in B \land B \in C) \to \exists x (A \in x \land x \in C)$
6		eluni	$⊢ A \in ⋃ C \leftrightarrow \exists x (A \in x \land x \in C)$
7	5 6	sylibr	$⊢ (A \in B \land B \in C) \to A \in ⋃ C$

Metamath Proof Explorer