Description: A set is a subset of the sigma-algebra it generates. (Contributed by Glauco Siliprandi, 3-Jan-2021)
Ref | Expression | ||
---|---|---|---|
Hypothesis | sssalgen.1 | |
|
Assertion | sssalgen | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sssalgen.1 | |
|
2 | ssint | |
|
3 | unieq | |
|
4 | 3 | eqeq1d | |
5 | sseq2 | |
|
6 | 4 5 | anbi12d | |
7 | 6 | elrab | |
8 | 7 | biimpi | |
9 | 8 | simprrd | |
10 | 2 9 | mprgbir | |
11 | 10 | a1i | |
12 | salgenval | |
|
13 | 1 12 | eqtr2id | |
14 | 11 13 | sseqtrd | |