elint

Description: Membership in class intersection. (Contributed by NM, 21-May-1994)

		Ref	Expression
	Hypothesis	elint.1	$⊢ A \in V$
	Assertion	elint	$⊢ A \in ⋂ B \leftrightarrow \forall x (x \in B \to A \in x)$

Step	Hyp	Ref	Expression
1		elint.1	$⊢ A \in V$
2		eleq1	$⊢ y = A \to (y \in x \leftrightarrow A \in x)$
3	2	imbi2d	$⊢ y = A \to ((x \in B \to y \in x) \leftrightarrow (x \in B \to A \in x))$
4	3	albidv	$⊢ y = A \to (\forall x (x \in B \to y \in x) \leftrightarrow \forall x (x \in B \to A \in x))$
5		df-int	$⊢ ⋂ B = \{y \| \forall x (x \in B \to y \in x)\}$
6	4 5	elab2g	$⊢ A \in V \to (A \in ⋂ B \leftrightarrow \forall x (x \in B \to A \in x))$
7	1 6	ax-mp	$⊢ A \in ⋂ B \leftrightarrow \forall x (x \in B \to A \in x)$

Metamath Proof Explorer