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