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

Theorem wunss 9740
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 9735 . . 3 (𝜑 → 𝒫 𝐴𝑈)
41, 3wunelss 9736 . 2 (𝜑 → 𝒫 𝐴𝑈)
5 wunss.3 . . 3 (𝜑𝐵𝐴)
62, 5sselpwd 4942 . 2 (𝜑𝐵 ∈ 𝒫 𝐴)
74, 6sseldd 3753 1 (𝜑𝐵𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2145  wss 3723  𝒫 cpw 4298  WUnicwun 9728
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1870  ax-4 1885  ax-5 1991  ax-6 2057  ax-7 2093  ax-9 2154  ax-10 2174  ax-11 2190  ax-12 2203  ax-13 2408  ax-ext 2751  ax-sep 4916
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 837  df-3an 1073  df-tru 1634  df-ex 1853  df-nf 1858  df-sb 2050  df-clab 2758  df-cleq 2764  df-clel 2767  df-nfc 2902  df-ne 2944  df-ral 3066  df-rex 3067  df-v 3353  df-in 3730  df-ss 3737  df-pw 4300  df-uni 4576  df-tr 4888  df-wun 9730
This theorem is referenced by:  wunin  9741  wundif  9742  wunint  9743  wun0  9746  wunom  9748  wunxp  9752  wunpm  9753  wunmap  9754  wundm  9756  wunrn  9757  wuncnv  9758  wunres  9759  wunfv  9760  wunco  9761  wuntpos  9762  wuncn  10197  wunndx  16085  wunstr  16088  wunfunc  16766
  Copyright terms: Public domain W3C validator