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

Metamath Proof Explorer

Theorem iinssiin

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

Ref Expression
Hypotheses iinssiin.1 
|- F/ x ph
iinssiin.2 
|- ( ( ph /\ x e. A ) -> B C_ C )
Assertion iinssiin 
|- ( ph -> |^|_ x e. A B C_ |^|_ x e. A C )

Proof

Step Hyp Ref Expression
1 iinssiin.1 
 |-  F/ x ph
2 iinssiin.2 
 |-  ( ( ph /\ x e. A ) -> B C_ C )
3 nfii1 
 |-  F/_ x |^|_ x e. A B
4 3 nfcri 
 |-  F/ x y e. |^|_ x e. A B
5 1 4 nfan 
 |-  F/ x ( ph /\ y e. |^|_ x e. A B )
6 2 adantlr 
 |-  ( ( ( ph /\ y e. |^|_ x e. A B ) /\ x e. A ) -> B C_ C )
7 eliinid 
 |-  ( ( y e. |^|_ x e. A B /\ x e. A ) -> y e. B )
8 7 adantll 
 |-  ( ( ( ph /\ y e. |^|_ x e. A B ) /\ x e. A ) -> y e. B )
9 6 8 sseldd 
 |-  ( ( ( ph /\ y e. |^|_ x e. A B ) /\ x e. A ) -> y e. C )
10 9 ex 
 |-  ( ( ph /\ y e. |^|_ x e. A B ) -> ( x e. A -> y e. C ) )
11 5 10 ralrimi 
 |-  ( ( ph /\ y e. |^|_ x e. A B ) -> A. x e. A y e. C )
12 eliin 
 |-  ( y e. _V -> ( y e. |^|_ x e. A C <-> A. x e. A y e. C ) )
13 12 elv 
 |-  ( y e. |^|_ x e. A C <-> A. x e. A y e. C )
14 11 13 sylibr 
 |-  ( ( ph /\ y e. |^|_ x e. A B ) -> y e. |^|_ x e. A C )
15 14 ssd 
 |-  ( ph -> |^|_ x e. A B C_ |^|_ x e. A C )