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

Theorem wunpw 9106
 Description: A weak universe is closed under powerset. (Contributed by Mario Carneiro, 2-Jan-2017.)
Hypotheses
Ref Expression
wununi.1
wununi.2
Assertion
Ref Expression
wunpw

Proof of Theorem wunpw
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 wununi.2 . 2
2 wununi.1 . . 3
3 iswun 9103 . . . . 5
43ibi 241 . . . 4
54simp3d 1010 . . 3
6 simp2 997 . . . 4
76ralimi 2850 . . 3
82, 5, 73syl 20 . 2
9 pweq 4015 . . . 4
109eleq1d 2526 . . 3
1110rspcv 3206 . 2
121, 8, 11sylc 60 1
 Colors of variables: wff setvar class Syntax hints:  ->wi 4  /\w3a 973  =wceq 1395  e.wcel 1818  =/=wne 2652  A.wral 2807   c0 3784  ~Pcpw 4012  {cpr 4031  U.cuni 4249  Trwtr 4545   cwun 9099 This theorem is referenced by:  wunss  9111  wunr1om  9118  wunxp  9123  wunpm  9124  intwun  9134  r1wunlim  9136  wuncval2  9146  wuncn  9568  wunfunc  15268  wunnat  15325  catcoppccl  15435  catcfuccl  15436  catcxpccl  15476 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435 This theorem depends on definitions:  df-bi 185  df-an 371  df-3an 975  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ne 2654  df-ral 2812  df-rex 2813  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014  df-uni 4250  df-tr 4546  df-wun 9101
 Copyright terms: Public domain W3C validator