| Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
| Mirrors > Home > MPE Home > Th. List > wunss | Structured version Visualization version GIF version | ||
| Description: A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.) |
| Ref | Expression |
|---|---|
| wununi.1 | ⊢ (𝜑 → 𝑈 ∈ WUni) |
| wununi.2 | ⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| wunss.3 | ⊢ (𝜑 → 𝐵 ⊆ 𝐴) |
| Ref | Expression |
|---|---|
| wunss | ⊢ (𝜑 → 𝐵 ∈ 𝑈) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | wununi.1 | . . 3 ⊢ (𝜑 → 𝑈 ∈ WUni) | |
| 2 | wununi.2 | . . . 4 ⊢ (𝜑 → 𝐴 ∈ 𝑈) | |
| 3 | 1, 2 | wunpw 10747 | . . 3 ⊢ (𝜑 → 𝒫 𝐴 ∈ 𝑈) |
| 4 | 1, 3 | wunelss 10748 | . 2 ⊢ (𝜑 → 𝒫 𝐴 ⊆ 𝑈) |
| 5 | wunss.3 | . . 3 ⊢ (𝜑 → 𝐵 ⊆ 𝐴) | |
| 6 | 2, 5 | sselpwd 5328 | . 2 ⊢ (𝜑 → 𝐵 ∈ 𝒫 𝐴) |
| 7 | 4, 6 | sseldd 3984 | 1 ⊢ (𝜑 → 𝐵 ∈ 𝑈) |
| Colors of variables: wff setvar class |
| Syntax hints: → wi 4 ∈ wcel 2108 ⊆ wss 3951 𝒫 cpw 4600 WUnicwun 10740 |
| This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1910 ax-6 1967 ax-7 2007 ax-8 2110 ax-9 2118 ax-ext 2708 ax-sep 5296 |
| This theorem depends on definitions: df-bi 207 df-an 396 df-3an 1089 df-tru 1543 df-ex 1780 df-sb 2065 df-clab 2715 df-cleq 2729 df-clel 2816 df-ne 2941 df-ral 3062 df-rex 3071 df-rab 3437 df-v 3482 df-in 3958 df-ss 3968 df-pw 4602 df-uni 4908 df-tr 5260 df-wun 10742 |
| This theorem is referenced by: wunin 10753 wundif 10754 wunint 10755 wun0 10758 wunom 10760 wunxp 10764 wunpm 10765 wunmap 10766 wundm 10768 wunrn 10769 wuncnv 10770 wunres 10771 wunfv 10772 wunco 10773 wuntpos 10774 wuncn 11210 wunstr 17225 wunndx 17232 wunfunc 17946 |
| Copyright terms: Public domain | W3C validator |