Theorem riinn0

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

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

Proof

Step	Hyp	Ref	Expression
1		incom	|- ( A i^i |^|_ x e. X S ) = ( |^|_ x e. X S i^i A )
2		r19.2z	|- ( ( X =/= (/) /\ A. x e. X S C_ A ) -> E. x e. X S C_ A )
3	2	ancoms	|- ( ( A. x e. X S C_ A /\ X =/= (/) ) -> E. x e. X S C_ A )
4		iinss	|- ( E. x e. X S C_ A -> |^|_ x e. X S C_ A )
5	3 4	syl	|- ( ( A. x e. X S C_ A /\ X =/= (/) ) -> |^|_ x e. X S C_ A )
6		df-ss	|- ( |^|_ x e. X S C_ A <-> ( |^|_ x e. X S i^i A ) = |^|_ x e. X S )
7	5 6	sylib	|- ( ( A. x e. X S C_ A /\ X =/= (/) ) -> ( |^|_ x e. X S i^i A ) = |^|_ x e. X S )
8	1 7	syl5eq	|- ( ( A. x e. X S C_ A /\ X =/= (/) ) -> ( A i^i |^|_ x e. X S ) = |^|_ x e. X S )