This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 dfss2 
 |-  ( |^|_ 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 )