Metamath Proof Explorer


Theorem iinssd

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

Ref Expression
Hypotheses iinssd.1
|- ( ph -> X e. A )
iinssd.2
|- ( x = X -> B = D )
iinssd.3
|- ( ph -> D C_ C )
Assertion iinssd
|- ( ph -> |^|_ x e. A B C_ C )

Proof

Step Hyp Ref Expression
1 iinssd.1
 |-  ( ph -> X e. A )
2 iinssd.2
 |-  ( x = X -> B = D )
3 iinssd.3
 |-  ( ph -> D C_ C )
4 2 sseq1d
 |-  ( x = X -> ( B C_ C <-> D C_ C ) )
5 4 rspcev
 |-  ( ( X e. A /\ D C_ C ) -> E. x e. A B C_ C )
6 1 3 5 syl2anc
 |-  ( ph -> E. x e. A B C_ C )
7 iinss
 |-  ( E. x e. A B C_ C -> |^|_ x e. A B C_ C )
8 6 7 syl
 |-  ( ph -> |^|_ x e. A B C_ C )