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