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

Metamath Proof Explorer

Theorem iinss

Description: Subset implication for an indexed intersection. (Contributed by NM, 15-Oct-2003) (Proof shortened by Andrew Salmon, 25-Jul-2011)

Ref Expression
Assertion iinss 
|- ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )

Proof

Step Hyp Ref Expression
1 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
2 1 elv 
 |-  ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
3 ssel 
 |-  ( B C_ C -> ( y e. B -> y e. C ) )
4 3 reximi 
 |-  ( E. x e. A B C_ C -> E. x e. A ( y e. B -> y e. C ) )
5 r19.36v 
 |-  ( E. x e. A ( y e. B -> y e. C ) -> ( A. x e. A y e. B -> y e. C ) )
6 4 5 syl 
 |-  ( E. x e. A B C_ C -> ( A. x e. A y e. B -> y e. C ) )
7 2 6 biimtrid 
 |-  ( E. x e. A B C_ C -> ( y e. |^|_ x e. A B -> y e. C ) )
8 7 ssrdv 
 |-  ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )