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

Theorem wunss 9038
Description: A weak universe is closed under subsets. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wununi.1  |-  ( ph  ->  U  e. WUni )
wununi.2  |-  ( ph  ->  A  e.  U )
wunss.3  |-  ( ph  ->  B  C_  A )
Assertion
Ref Expression
wunss  |-  ( ph  ->  B  e.  U )

Proof of Theorem wunss
StepHypRef Expression
1 wununi.1 . . 3  |-  ( ph  ->  U  e. WUni )
2 wununi.2 . . . 4  |-  ( ph  ->  A  e.  U )
31, 2wunpw 9033 . . 3  |-  ( ph  ->  ~P A  e.  U
)
41, 3wunelss 9034 . 2  |-  ( ph  ->  ~P A  C_  U
)
5 wunss.3 . . 3  |-  ( ph  ->  B  C_  A )
6 elpw2g 4554 . . . 4  |-  ( A  e.  U  ->  ( B  e.  ~P A  <->  B 
C_  A ) )
72, 6syl 17 . . 3  |-  ( ph  ->  ( B  e.  ~P A 
<->  B  C_  A )
)
85, 7mpbird 232 . 2  |-  ( ph  ->  B  e.  ~P A
)
94, 8sseldd 3440 1  |-  ( ph  ->  B  e.  U )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    e. wcel 1840    C_ wss 3411   ~Pcpw 3952  WUnicwun 9026
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1637  ax-4 1650  ax-5 1723  ax-6 1769  ax-7 1812  ax-10 1859  ax-11 1864  ax-12 1876  ax-13 2024  ax-ext 2378  ax-sep 4514
This theorem depends on definitions:  df-bi 185  df-an 369  df-3an 974  df-tru 1406  df-ex 1632  df-nf 1636  df-sb 1762  df-clab 2386  df-cleq 2392  df-clel 2395  df-nfc 2550  df-ne 2598  df-ral 2756  df-rex 2757  df-v 3058  df-in 3418  df-ss 3425  df-pw 3954  df-uni 4189  df-tr 4487  df-wun 9028
This theorem is referenced by:  wunin  9039  wundif  9040  wunint  9041  wun0  9044  wunom  9046  wunxp  9050  wunpm  9051  wunmap  9052  wundm  9054  wunrn  9055  wuncnv  9056  wunres  9057  wunfv  9058  wunco  9059  wuntpos  9060  wuncn  9495  wunndx  14747  wunstr  14750  wunfunc  15402
  Copyright terms: Public domain W3C validator