Metamath Proof Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >  wunss Structured version   Visualization version   GIF version

Theorem wunss 9413
 Description: A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wununi.1 (𝜑𝑈 ∈ WUni)
wununi.2 (𝜑𝐴𝑈)
wunss.3 (𝜑𝐵𝐴)
Assertion
Ref Expression
wunss (𝜑𝐵𝑈)

Proof of Theorem wunss
StepHypRef Expression
1 wununi.1 . . 3 (𝜑𝑈 ∈ WUni)
2 wununi.2 . . . 4 (𝜑𝐴𝑈)
31, 2wunpw 9408 . . 3 (𝜑 → 𝒫 𝐴𝑈)
41, 3wunelss 9409 . 2 (𝜑 → 𝒫 𝐴𝑈)
5 wunss.3 . . 3 (𝜑𝐵𝐴)
6 elpw2g 4754 . . . 4 (𝐴𝑈 → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
72, 6syl 17 . . 3 (𝜑 → (𝐵 ∈ 𝒫 𝐴𝐵𝐴))
85, 7mpbird 246 . 2 (𝜑𝐵 ∈ 𝒫 𝐴)
94, 8sseldd 3569 1 (𝜑𝐵𝑈)
 Colors of variables: wff setvar class Syntax hints:   → wi 4   ↔ wb 195   ∈ wcel 1977   ⊆ wss 3540  𝒫 cpw 4108  WUnicwun 9401 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590  ax-sep 4709 This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-3an 1033  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-ne 2782  df-ral 2901  df-rex 2902  df-v 3175  df-in 3547  df-ss 3554  df-pw 4110  df-uni 4373  df-tr 4681  df-wun 9403 This theorem is referenced by:  wunin  9414  wundif  9415  wunint  9416  wun0  9419  wunom  9421  wunxp  9425  wunpm  9426  wunmap  9427  wundm  9429  wunrn  9430  wuncnv  9431  wunres  9432  wunfv  9433  wunco  9434  wuntpos  9435  wuncn  9870  wunndx  15711  wunstr  15714  wunfunc  16382
 Copyright terms: Public domain W3C validator