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

Theorem wunss 9144
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 9139 . . 3  |-  ( ph  ->  ~P A  e.  U
)
41, 3wunelss 9140 . 2  |-  ( ph  ->  ~P A  C_  U
)
5 wunss.3 . . 3  |-  ( ph  ->  B  C_  A )
6 elpw2g 4587 . . . 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 235 . 2  |-  ( ph  ->  B  e.  ~P A
)
94, 8sseldd 3465 1  |-  ( ph  ->  B  e.  U )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 187    e. wcel 1872    C_ wss 3436   ~Pcpw 3981  WUnicwun 9132
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401  ax-sep 4546
This theorem depends on definitions:  df-bi 188  df-an 372  df-3an 984  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-ne 2616  df-ral 2776  df-rex 2777  df-v 3082  df-in 3443  df-ss 3450  df-pw 3983  df-uni 4220  df-tr 4519  df-wun 9134
This theorem is referenced by:  wunin  9145  wundif  9146  wunint  9147  wun0  9150  wunom  9152  wunxp  9156  wunpm  9157  wunmap  9158  wundm  9160  wunrn  9161  wuncnv  9162  wunres  9163  wunfv  9164  wunco  9165  wuntpos  9166  wuncn  9601  wunndx  15136  wunstr  15139  wunfunc  15803
  Copyright terms: Public domain W3C validator