Description: Express the predicate " S is a sigma-algebra." (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | issal | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | eleq2 | |
|
2 | id | |
|
3 | unieq | |
|
4 | 3 | difeq1d | |
5 | 4 2 | eleq12d | |
6 | 2 5 | raleqbidv | |
7 | pweq | |
|
8 | eleq2 | |
|
9 | 8 | imbi2d | |
10 | 7 9 | raleqbidv | |
11 | 1 6 10 | 3anbi123d | |
12 | df-salg | |
|
13 | 11 12 | elab2g | |