elintrabg

Description: Membership in the intersection of a class abstraction. (Contributed by NM, 17-Feb-2007)

		Ref	Expression
	Assertion	elintrabg	$⊢ A \in V \to (A \in ⋂ \{x \in B \| φ\} \leftrightarrow \forall x \in B (φ \to A \in x))$

Step	Hyp	Ref	Expression
1		eleq1	$⊢ y = A \to (y \in ⋂ \{x \in B \| φ\} \leftrightarrow A \in ⋂ \{x \in B \| φ\})$
2		eleq1	$⊢ y = A \to (y \in x \leftrightarrow A \in x)$
3	2	imbi2d	$⊢ y = A \to ((φ \to y \in x) \leftrightarrow (φ \to A \in x))$
4	3	ralbidv	$⊢ y = A \to (\forall x \in B (φ \to y \in x) \leftrightarrow \forall x \in B (φ \to A \in x))$
5		vex	$⊢ y \in V$
6	5	elintrab	$⊢ y \in ⋂ \{x \in B \| φ\} \leftrightarrow \forall x \in B (φ \to y \in x)$
7	1 4 6	vtoclbg	$⊢ A \in V \to (A \in ⋂ \{x \in B \| φ\} \leftrightarrow \forall x \in B (φ \to A \in x))$

Metamath Proof Explorer