![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > pwuni | Structured version Visualization version GIF version |
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 |
---|---|
pwuni | ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | elssuni 4937 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) | |
2 | velpw 4602 | . . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴) | |
3 | 1, 2 | sylibr 233 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴) |
4 | 3 | ssriv 3982 | 1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2099 ⊆ wss 3946 𝒫 cpw 4597 ∪ cuni 4905 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1790 ax-4 1804 ax-5 1906 ax-6 1964 ax-7 2004 ax-8 2101 ax-9 2109 ax-ext 2697 |
This theorem depends on definitions: df-bi 206 df-an 395 df-tru 1537 df-ex 1775 df-sb 2061 df-clab 2704 df-cleq 2718 df-clel 2803 df-v 3464 df-ss 3963 df-pw 4599 df-uni 4906 |
This theorem is referenced by: uniexr 7763 fipwuni 9462 uniwf 9855 rankuni 9899 rankc2 9907 rankxplim 9915 fin23lem17 10372 axcclem 10491 grurn 10835 istopon 22902 eltg3i 22952 cmpfi 23400 hmphdis 23788 ptcmpfi 23805 fbssfi 23829 mopnfss 24437 pliguhgr 30416 shsspwh 31176 circtopn 33665 hasheuni 33931 issgon 33969 sigaclci 33978 sigagenval 33986 dmsigagen 33990 imambfm 34109 bj-unirel 36771 salgenval 45978 salgenn0 45988 caragensspw 46166 |
Copyright terms: Public domain | W3C validator |