Theorem sspwuni 4055

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 2805	. . . 4 |- x e. _V
2	1	elpw 3658	. . 3 |- ( x e. ~P B <-> x C_ B )
3	2	ralbii 2538	. 2 |- ( A. x e. A x e. ~P B <-> A. x e. A x C_ B )
4		dfss3 3216	. 2 |- ( A C_ ~P B <-> A. x e. A x e. ~P B )
5		unissb 3923	. 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 2202   A.wral 2510   C_ wss 3200   ~Pcpw 3652   U.cuni 3893

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 716  ax-5 1495  ax-7 1496  ax-gen 1497  ax-ie1 1541  ax-ie2 1542  ax-8 1552  ax-10 1553  ax-11 1554  ax-i12 1555  ax-bndl 1557  ax-4 1558  ax-17 1574  ax-i9 1578  ax-ial 1582  ax-i5r 1583  ax-ext 2213

This theorem depends on definitions:  df-bi 117  df-tru 1400  df-nf 1509  df-sb 1811  df-clab 2218  df-cleq 2224  df-clel 2227  df-nfc 2363  df-ral 2515  df-v 2804  df-in 3206  df-ss 3213  df-pw 3654  df-uni 3894

This theorem is referenced by:  pwssb  4056  elpwpw  4057  elpwuni  4060  rintm  4063  dftr4  4192  iotass  5304  tfrlemibfn  6493  tfr1onlembfn  6509  tfrcllembfn  6522  uniixp  6889  fipwssg  7177  unirnioo  10207  restid  13332  lssintclm  14397  topgele  14752  topontopn  14760  unitg  14785  epttop  14813  resttopon  14894  txuni2  14979  txdis  15000  unirnblps  15145  unirnbl  15146