eliun

		Ref	Expression
	Assertion	eliun	$⊢ A \in ⋃_{x \in B} C \leftrightarrow \exists x \in B A \in C$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in ⋃_{x \in B} C \to A \in V$
2		elex	$⊢ A \in C \to A \in V$
3	2	rexlimivw	$⊢ \exists x \in B A \in C \to A \in V$
4		eleq1	$⊢ y = A \to (y \in C \leftrightarrow A \in C)$
5	4	rexbidv	$⊢ y = A \to (\exists x \in B y \in C \leftrightarrow \exists x \in B A \in C)$
6		df-iun	$⊢ ⋃_{x \in B} C = \{y \| \exists x \in B y \in C\}$
7	5 6	elab2g	$⊢ A \in V \to (A \in ⋃_{x \in B} C \leftrightarrow \exists x \in B A \in C)$
8	1 3 7	pm5.21nii	$⊢ A \in ⋃_{x \in B} C \leftrightarrow \exists x \in B A \in C$

Metamath Proof Explorer