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.

Step	Hyp	Ref	Expression
1		wununi.2	. 2
2		wununi.1	. . 3
3		iswun 9103	. . . . 5
4	3	ibi 241	. . . 4
5	4	simp3d 1010	. . 3
6		simp2 997	. . . 4
7	6	ralimi 2850	. . 3
8	2, 5, 7	3syl 20	. 2
9		pweq 4015	. . . 4
10	9	eleq1d 2526	. . 3
11	10	rspcv 3206	. 2
12	1, 8, 11	sylc 60	1

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