riinrab

Description: Relative intersection of a relative abstraction. (Contributed by Stefan O'Rear, 3-Apr-2015)

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

Step	Hyp	Ref	Expression
1		riin0	$⊢ X = \emptyset \to A \cap ⋂_{x \in X} \{y \in A \| φ\} = A$
2		rzal	$⊢ X = \emptyset \to \forall x \in X φ$
3	2	ralrimivw	$⊢ X = \emptyset \to \forall y \in A \forall x \in X φ$
4		rabid2	$⊢ A = \{y \in A \| \forall x \in X φ\} \leftrightarrow \forall y \in A \forall x \in X φ$
5	3 4	sylibr	$⊢ X = \emptyset \to A = \{y \in A \| \forall x \in X φ\}$
6	1 5	eqtrd	$⊢ X = \emptyset \to A \cap ⋂_{x \in X} \{y \in A \| φ\} = \{y \in A \| \forall x \in X φ\}$
7		ssrab2	$⊢ \{y \in A \| φ\} \subseteq A$
8	7	rgenw	$⊢ \forall x \in X \{y \in A \| φ\} \subseteq A$
9		riinn0	$⊢ (\forall x \in X \{y \in A \| φ\} \subseteq A \land X \neq \emptyset) \to A \cap ⋂_{x \in X} \{y \in A \| φ\} = ⋂_{x \in X} \{y \in A \| φ\}$
10	8 9	mpan	$⊢ X \neq \emptyset \to A \cap ⋂_{x \in X} \{y \in A \| φ\} = ⋂_{x \in X} \{y \in A \| φ\}$
11		iinrab	$⊢ X \neq \emptyset \to ⋂_{x \in X} \{y \in A \| φ\} = \{y \in A \| \forall x \in X φ\}$
12	10 11	eqtrd	$⊢ X \neq \emptyset \to A \cap ⋂_{x \in X} \{y \in A \| φ\} = \{y \in A \| \forall x \in X φ\}$
13	6 12	pm2.61ine	$⊢ A \cap ⋂_{x \in X} \{y \in A \| φ\} = \{y \in A \| \forall x \in X φ\}$

Metamath Proof Explorer