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

Metamath Proof Explorer

Theorem ssiinf

Description: Subset theorem for an indexed intersection. (Contributed by FL, 15-Oct-2012) (Proof shortened by Mario Carneiro, 14-Oct-2016)

Ref Expression
Hypothesis ssiinf.1 
|- F/_ x C
Assertion ssiinf 
|- ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )

Proof

Step Hyp Ref Expression
1 ssiinf.1 
 |-  F/_ x C
2 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A B <-> A. x e. A y e. B ) )
3 2 elv 
 |-  ( y e. |^|_ x e. A B <-> A. x e. A y e. B )
4 3 ralbii 
 |-  ( A. y e. C y e. |^|_ x e. A B <-> A. y e. C A. x e. A y e. B )
5 nfcv 
 |-  F/_ y A
6 1 5 ralcomf 
 |-  ( A. y e. C A. x e. A y e. B <-> A. x e. A A. y e. C y e. B )
7 4 6 bitri 
 |-  ( A. y e. C y e. |^|_ x e. A B <-> A. x e. A A. y e. C y e. B )
8 dfss3 
 |-  ( C C_ |^|_ x e. A B <-> A. y e. C y e. |^|_ x e. A B )
9 dfss3 
 |-  ( C C_ B <-> A. y e. C y e. B )
10 9 ralbii 
 |-  ( A. x e. A C C_ B <-> A. x e. A A. y e. C y e. B )
11 7 8 10 3bitr4i 
 |-  ( C C_ |^|_ x e. A B <-> A. x e. A C C_ B )