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	3 4	cleqf	$⊢ ⋂_{x \in A} \{y \| φ\} = \{y \| \forall x \in A φ\} \leftrightarrow \forall y (y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow y \in \{y \| \forall x \in A φ\})$
6		abid	$⊢ y \in \{y \| φ\} \leftrightarrow φ$
7	6	ralbii	$⊢ \forall x \in A y \in \{y \| φ\} \leftrightarrow \forall x \in A φ$
8		eliin	$⊢ y \in V \to (y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow \forall x \in A y \in \{y \| φ\})$
9	8	elv	$⊢ y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow \forall x \in A y \in \{y \| φ\}$
10		abid	$⊢ y \in \{y \| \forall x \in A φ\} \leftrightarrow \forall x \in A φ$
11	7 9 10	3bitr4i	$⊢ y \in ⋂_{x \in A} \{y \| φ\} \leftrightarrow y \in \{y \| \forall x \in A φ\}$
12	5 11	mpgbir	$⊢ ⋂_{x \in A} \{y \| φ\} = \{y \| \forall x \in A φ\}$

Metamath Proof Explorer