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

Theorem wunss 10350
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 10345 . . 3 (𝜑 → 𝒫 𝐴𝑈)
41, 3wunelss 10346 . 2 (𝜑 → 𝒫 𝐴𝑈)
5 wunss.3 . . 3 (𝜑𝐵𝐴)
62, 5sselpwd 5233 . 2 (𝜑𝐵 ∈ 𝒫 𝐴)
74, 6sseldd 3916 1 (𝜑𝐵𝑈)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2111  wss 3880  𝒫 cpw 4527  WUnicwun 10338
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 2113  ax-9 2121  ax-11 2159  ax-ext 2709  ax-sep 5206
This theorem depends on definitions:  df-bi 210  df-an 400  df-3an 1091  df-tru 1546  df-ex 1788  df-sb 2072  df-clab 2716  df-cleq 2730  df-clel 2817  df-ne 2942  df-ral 3067  df-rab 3071  df-v 3422  df-in 3887  df-ss 3897  df-pw 4529  df-uni 4834  df-tr 5176  df-wun 10340
This theorem is referenced by:  wunin  10351  wundif  10352  wunint  10353  wun0  10356  wunom  10358  wunxp  10362  wunpm  10363  wunmap  10364  wundm  10366  wunrn  10367  wuncnv  10368  wunres  10369  wunfv  10370  wunco  10371  wuntpos  10372  wuncn  10808  wunstr  16765  wunndx  16770  wunfunc  17429  wunfuncOLD  17430
  Copyright terms: Public domain W3C validator