Description: Relationship between power class and union. (Contributed by Glauco Siliprandi, 17-Aug-2020)
Ref | Expression | ||
---|---|---|---|
Assertion | pwpwuni |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elpwg | ||
2 | sspwuni | ||
3 | 2 | a1i | |
4 | uniexg | ||
5 | elpwg | ||
6 | 4 5 | syl | |
7 | 6 | bicomd | |
8 | 1 3 7 | 3bitrd |