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 ) |
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 ) |