iinrab

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

		Ref	Expression
	Assertion	iinrab	$⊢ A \neq \emptyset \to ⋂_{x \in A} \{y \in B \| φ\} = \{y \in B \| \forall x \in A φ\}$

Step	Hyp	Ref	Expression
1		r19.28zv	$⊢ A \neq \emptyset \to (\forall x \in A (y \in B \land φ) \leftrightarrow (y \in B \land \forall x \in A φ))$
2	1	abbidv	$⊢ A \neq \emptyset \to \{y \| \forall x \in A (y \in B \land φ)\} = \{y \| (y \in B \land \forall x \in A φ)\}$
3		df-rab	$⊢ \{y \in B \| φ\} = \{y \| (y \in B \land φ)\}$
4	3	a1i	$⊢ x \in A \to \{y \in B \| φ\} = \{y \| (y \in B \land φ)\}$
5	4	iineq2i	$⊢ ⋂_{x \in A} \{y \in B \| φ\} = ⋂_{x \in A} \{y \| (y \in B \land φ)\}$
6		iinab	$⊢ ⋂_{x \in A} \{y \| (y \in B \land φ)\} = \{y \| \forall x \in A (y \in B \land φ)\}$
7	5 6	eqtri	$⊢ ⋂_{x \in A} \{y \in B \| φ\} = \{y \| \forall x \in A (y \in B \land φ)\}$
8		df-rab	$⊢ \{y \in B \| \forall x \in A φ\} = \{y \| (y \in B \land \forall x \in A φ)\}$
9	2 7 8	3eqtr4g	$⊢ A \neq \emptyset \to ⋂_{x \in A} \{y \in B \| φ\} = \{y \in B \| \forall x \in A φ\}$

Metamath Proof Explorer