iinab

Description: Indexed intersection of a class abstraction. (Contributed by NM, 6-Dec-2011)

		Ref	Expression
	Assertion	iinab	$⊢ ⋂_{x \in A} \{y \| φ\} = \{y \| \forall x \in A φ\}$

Step	Hyp	Ref	Expression
1		nfcv	$⊢ \underline{Ⅎ} y A$
2		nfab1	$⊢ \underline{Ⅎ} y \{y \| φ\}$
3	1 2	nfiin	$⊢ \underline{Ⅎ} y ⋂_{x \in A} \{y \| φ\}$
4		nfab1	$⊢ \underline{Ⅎ} y \{y \| \forall x \in A φ\}$
5		abid	$⊢ y \in \{y \| φ\} \leftrightarrow φ$
6	5	ralbii	$⊢ \forall x \in A y \in \{y \| φ\} \leftrightarrow \forall x \in A φ$
7		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow \forall x \in A y \in \{y \| φ\})$
8	7	elv	$⊢ y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow \forall x \in A y \in \{y \| φ\}$
9		abid	$⊢ y \in \{y \| \forall x \in A φ\} \leftrightarrow \forall x \in A φ$
10	6 8 9	3bitr4i	$⊢ y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow y \in \{y \| \forall x \in A φ\}$
11	3 4 10	eqri	$⊢ ⋂_{x \in A} \{y \| φ\} = \{y \| \forall x \in A φ\}$

Metamath Proof Explorer