eluni

		Ref	Expression
	Assertion	eluni	$⊢ A \in ⋃ B \leftrightarrow \exists x (A \in x \land x \in B)$

Step	Hyp	Ref	Expression
1		elex	$⊢ A \in ⋃ B \to A \in V$
2		elex	$⊢ A \in x \to A \in V$
3	2	adantr	$⊢ (A \in x \land x \in B) \to A \in V$
4	3	exlimiv	$⊢ \exists x (A \in x \land x \in B) \to A \in V$
5		eleq1	$⊢ y = A \to (y \in x \leftrightarrow A \in x)$
6	5	anbi1d	$⊢ y = A \to ((y \in x \land x \in B) \leftrightarrow (A \in x \land x \in B))$
7	6	exbidv	$⊢ y = A \to (\exists x (y \in x \land x \in B) \leftrightarrow \exists x (A \in x \land x \in B))$
8		df-uni	$⊢ ⋃ B = \{y \| \exists x (y \in x \land x \in B)\}$
9	7 8	elab2g	$⊢ A \in V \to (A \in ⋃ B \leftrightarrow \exists x (A \in x \land x \in B))$
10	1 4 9	pm5.21nii	$⊢ A \in ⋃ B \leftrightarrow \exists x (A \in x \land x \in B)$

Metamath Proof Explorer