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

Metamath Proof Explorer

Theorem iinssf

Description: Subset implication for an indexed intersection. (Contributed by Glauco Siliprandi, 23-Oct-2021)

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

Proof

Step Hyp Ref Expression
1 iinssf.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 ssel 
 |-  ( B C_ C -> ( y e. B -> y e. C ) )
5 4 reximi 
 |-  ( E. x e. A B C_ C -> E. x e. A ( y e. B -> y e. C ) )
6 1 nfcri 
 |-  F/ x y e. C
7 6 r19.36vf 
 |-  ( E. x e. A ( y e. B -> y e. C ) -> ( A. x e. A y e. B -> y e. C ) )
8 5 7 syl 
 |-  ( E. x e. A B C_ C -> ( A. x e. A y e. B -> y e. C ) )
9 3 8 biimtrid 
 |-  ( E. x e. A B C_ C -> ( y e. |^|_ x e. A B -> y e. C ) )
10 9 ssrdv 
 |-  ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )