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 4851 | . . 3 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ⊆ ∪ 𝐴) | |
2 | velpw 4518 | . . 3 ⊢ (𝑥 ∈ 𝒫 ∪ 𝐴 ↔ 𝑥 ⊆ ∪ 𝐴) | |
3 | 1, 2 | sylibr 237 | . 2 ⊢ (𝑥 ∈ 𝐴 → 𝑥 ∈ 𝒫 ∪ 𝐴) |
4 | 3 | ssriv 3905 | 1 ⊢ 𝐴 ⊆ 𝒫 ∪ 𝐴 |
Colors of variables: wff setvar class |
Syntax hints: ∈ wcel 2110 ⊆ wss 3866 𝒫 cpw 4513 ∪ cuni 4819 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1803 ax-4 1817 ax-5 1918 ax-6 1976 ax-7 2016 ax-8 2112 ax-9 2120 ax-ext 2708 |
This theorem depends on definitions: df-bi 210 df-an 400 df-tru 1546 df-ex 1788 df-sb 2071 df-clab 2715 df-cleq 2729 df-clel 2816 df-v 3410 df-in 3873 df-ss 3883 df-pw 4515 df-uni 4820 |
This theorem is referenced by: uniexr 7548 fipwuni 9042 uniwf 9435 rankuni 9479 rankc2 9487 rankxplim 9495 fin23lem17 9952 axcclem 10071 grurn 10415 istopon 21809 eltg3i 21858 cmpfi 22305 hmphdis 22693 ptcmpfi 22710 fbssfi 22734 mopnfss 23341 pliguhgr 28567 shsspwh 29327 circtopn 31501 hasheuni 31765 issgon 31803 sigaclci 31812 sigagenval 31820 dmsigagen 31824 imambfm 31941 bj-unirel 34961 salgenval 43537 salgenn0 43545 caragensspw 43722 |
Copyright terms: Public domain | W3C validator |