Theorem riin0

Description: Relative intersection of an empty family. (Contributed by Stefan O'Rear, 3-Apr-2015)

	Ref	Expression
Assertion	riin0	|- ( X = (/) -> ( A i^i |^|_ x e. X S ) = A )

Proof

Step	Hyp	Ref	Expression
1		iineq1	|- ( X = (/) -> |^|_ x e. X S = |^|_ x e. (/) S )
2	1	ineq2d	|- ( X = (/) -> ( A i^i |^|_ x e. X S ) = ( A i^i |^|_ x e. (/) S ) )
3		0iin	|- |^|_ x e. (/) S = _V
4	3	ineq2i	|- ( A i^i |^|_ x e. (/) S ) = ( A i^i _V )
5		inv1	|- ( A i^i _V ) = A
6	4 5	eqtri	|- ( A i^i |^|_ x e. (/) S ) = A
7	2 6	eqtrdi	|- ( X = (/) -> ( A i^i |^|_ x e. X S ) = A )