Theorem sspwuni 4076

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 2816	. . . 4 |- x e. _V
2	1	elpw 3675	. . 3 |- ( x e. ~P B <-> x C_ B )
3	2	ralbii 2548	. 2 |- ( A. x e. A x e. ~P B <-> A. x e. A x C_ B )
4		dfss3 3227	. 2 |- ( A C_ ~P B <-> A. x e. A x e. ~P B )
5		unissb 3944	. 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 2203   A.wral 2520   C_ wss 3211   ~Pcpw 3669   U.cuni 3914

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 717  ax-5 1496  ax-7 1497  ax-gen 1498  ax-ie1 1542  ax-ie2 1543  ax-8 1553  ax-10 1554  ax-11 1555  ax-i12 1556  ax-bndl 1558  ax-4 1559  ax-17 1575  ax-i9 1579  ax-ial 1583  ax-i5r 1584  ax-ext 2214

This theorem depends on definitions:  df-bi 117  df-tru 1401  df-nf 1510  df-sb 1812  df-clab 2219  df-cleq 2225  df-clel 2228  df-nfc 2373  df-ral 2525  df-v 2815  df-in 3217  df-ss 3224  df-pw 3671  df-uni 3915

This theorem is referenced by:  pwssb  4077  elpwpw  4078  elpwuni  4081  rintm  4084  dftr4  4213  iotass  5330  tfrlemibfn  6559  tfr1onlembfn  6575  tfrcllembfn  6588  uniixp  6956  fipwssg  7266  unirnioo  10306  restid  13463  lssintclm  14532  topgele  14894  topontopn  14902  unitg  14927  epttop  14955  resttopon  15036  txuni2  15121  txdis  15142  unirnblps  15287  unirnbl  15288