Metamath Proof Explorer


Theorem iinssdf

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

Ref Expression
Hypotheses iinssdf.a
|- F/_ x A
iinssdf.n
|- F/_ x X
iinssdf.c
|- F/_ x C
iinssdf.d
|- F/_ x D
iinssdf.x
|- ( ph -> X e. A )
iinssdf.b
|- ( x = X -> B = D )
iinssdf.s
|- ( ph -> D C_ C )
Assertion iinssdf
|- ( ph -> |^|_ x e. A B C_ C )

Proof

Step Hyp Ref Expression
1 iinssdf.a
 |-  F/_ x A
2 iinssdf.n
 |-  F/_ x X
3 iinssdf.c
 |-  F/_ x C
4 iinssdf.d
 |-  F/_ x D
5 iinssdf.x
 |-  ( ph -> X e. A )
6 iinssdf.b
 |-  ( x = X -> B = D )
7 iinssdf.s
 |-  ( ph -> D C_ C )
8 4 3 nfss
 |-  F/ x D C_ C
9 6 sseq1d
 |-  ( x = X -> ( B C_ C <-> D C_ C ) )
10 8 2 1 9 rspcef
 |-  ( ( X e. A /\ D C_ C ) -> E. x e. A B C_ C )
11 5 7 10 syl2anc
 |-  ( ph -> E. x e. A B C_ C )
12 3 iinssf
 |-  ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
13 11 12 syl
 |-  ( ph -> |^|_ x e. A B C_ C )