Theorem viin

Description: Indexed intersection with a universal index class. When A doesn't depend on x , this evaluates to A by 19.3 and abid2 . When A = x , this evaluates to (/) by intiin and intv . (Contributed by NM, 11-Sep-2008)

	Ref	Expression
Assertion	viin	|- |^|_ x e. _V A = { y | A. x y e. A }

Proof

Step	Hyp	Ref	Expression
1		df-iin	|- |^|_ x e. _V A = { y | A. x e. _V y e. A }
2		ralv	|- ( A. x e. _V y e. A <-> A. x y e. A )
3	2	abbii	|- { y | A. x e. _V y e. A } = { y | A. x y e. A }
4	1 3	eqtri	|- |^|_ x e. _V A = { y | A. x y e. A }