Metamath Proof Explorer


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 eqtrid
 |-  ( ( A. x e. X S C_ A /\ X =/= (/) ) -> ( A i^i |^|_ x e. X S ) = |^|_ x e. X S )