Theorem sspwuni 3985

Description: Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)

Assertion

Ref	Expression
sspwuni	|- ( A C_ ~P B <-> U. A C_ B )

Proof of Theorem sspwuni

Dummy variable x is distinct from all other variables.

Step	Hyp	Ref	Expression
1		vex 2754	. . . 4 |- x e. _V
2	1	elpw 3595	. . 3 |- ( x e. ~P B <-> x C_ B )
3	2	ralbii 2495	. 2 |- ( A. x e. A x e. ~P B <-> A. x e. A x C_ B )
4		dfss3 3159	. 2 |- ( A C_ ~P B <-> A. x e. A x e. ~P B )
5		unissb 3853	. 2 |- ( U. A C_ B <-> A. x e. A x C_ B )
6	3, 4, 5	3bitr4i 212	1 |- ( A C_ ~P B <-> U. A C_ B )

Syntax hints:   <-> wb 105   e. wcel 2159   A.wral 2467   C_ wss 3143   ~Pcpw 3589   U.cuni 3823

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 710  ax-5 1457  ax-7 1458  ax-gen 1459  ax-ie1 1503  ax-ie2 1504  ax-8 1514  ax-10 1515  ax-11 1516  ax-i12 1517  ax-bndl 1519  ax-4 1520  ax-17 1536  ax-i9 1540  ax-ial 1544  ax-i5r 1545  ax-ext 2170

This theorem depends on definitions:  df-bi 117  df-tru 1366  df-nf 1471  df-sb 1773  df-clab 2175  df-cleq 2181  df-clel 2184  df-nfc 2320  df-ral 2472  df-v 2753  df-in 3149  df-ss 3156  df-pw 3591  df-uni 3824

This theorem is referenced by:  pwssb  3986  elpwpw  3987  elpwuni  3990  rintm  3993  dftr4  4120  iotass  5209  tfrlemibfn  6346  tfr1onlembfn  6362  tfrcllembfn  6375  uniixp  6738  fipwssg  6995  unirnioo  9990  restid  12720  lssintclm  13660  topgele  13912  topontopn  13920  unitg  13945  epttop  13973  resttopon  14054  txuni2  14139  txdis  14160  unirnblps  14305  unirnbl  14306