Description: Quantitative version of pwexg : the powerset of an element of a class is an element of the double powerclass of the union of that class. Exercise 10 of Enderton p. 26. (Contributed by NM, 13-Jan-2007) Remove use of ax-nul and ax-pr and shorten proof. (Revised by BJ, 13-Apr-2024)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | pwel | |- ( A e. B -> ~P A e. ~P ~P U. B ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | pwexg | |- ( A e. B -> ~P A e. _V ) |
|
| 2 | elssuni | |- ( A e. B -> A C_ U. B ) |
|
| 3 | 2 | sspwd | |- ( A e. B -> ~P A C_ ~P U. B ) |
| 4 | 1 3 | elpwd | |- ( A e. B -> ~P A e. ~P ~P U. B ) |