elunirab

Description: Membership in union of a class abstraction. (Contributed by NM, 4-Oct-2006)

		Ref	Expression
	Assertion	elunirab	$⊢ A \in ⋃ \{x \in B \| φ\} \leftrightarrow \exists x \in B (A \in x \land φ)$

Step	Hyp	Ref	Expression
1		eluniab	$⊢ A \in ⋃ \{x \| (x \in B \land φ)\} \leftrightarrow \exists x (A \in x \land (x \in B \land φ))$
2		df-rab	$⊢ \{x \in B \| φ\} = \{x \| (x \in B \land φ)\}$
3	2	unieqi	$⊢ ⋃ \{x \in B \| φ\} = ⋃ \{x \| (x \in B \land φ)\}$
4	3	eleq2i	$⊢ A \in ⋃ \{x \in B \| φ\} \leftrightarrow A \in ⋃ \{x \| (x \in B \land φ)\}$
5		df-rex	$⊢ \exists x \in B (A \in x \land φ) \leftrightarrow \exists x (x \in B \land (A \in x \land φ))$
6		an12	$⊢ (x \in B \land (A \in x \land φ)) \leftrightarrow (A \in x \land (x \in B \land φ))$
7	6	exbii	$⊢ \exists x (x \in B \land (A \in x \land φ)) \leftrightarrow \exists x (A \in x \land (x \in B \land φ))$
8	5 7	bitri	$⊢ \exists x \in B (A \in x \land φ) \leftrightarrow \exists x (A \in x \land (x \in B \land φ))$
9	1 4 8	3bitr4i	$⊢ A \in ⋃ \{x \in B \| φ\} \leftrightarrow \exists x \in B (A \in x \land φ)$

Metamath Proof Explorer