Description: A class is a subclass of the power class of its union. Exercise 6(b) of Enderton p. 38. (Contributed by NM, 14-Oct-1996)
Ref | Expression | ||
---|---|---|---|
Assertion | pwuni | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elssuni | |
|
2 | velpw | |
|
3 | 1 2 | sylibr | |
4 | 3 | ssriv | |