Theorem sspwuni 4611

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		selpw 4165	. . 3 |- ( x e. ~P B <-> x C_ B )
2	1	ralbii 2980	. 2 |- ( A. x e. A x e. ~P B <-> A. x e. A x C_ B )
3		dfss3 3592	. 2 |- ( A C_ ~P B <-> A. x e. A x e. ~P B )
4		unissb 4469	. 2 |- ( U. A C_ B <-> A. x e. A x C_ B )
5	2, 3, 4	3bitr4i 292	1 |- ( A C_ ~P B <-> U. A C_ B )

Syntax hints:   <-> wb 196   e. wcel 1990   A.wral 2912   C_ wss 3574   ~Pcpw 4158   U.cuni 4436

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-ral 2917  df-v 3202  df-in 3581  df-ss 3588  df-pw 4160  df-uni 4437

This theorem is referenced by:  pwssb  4612  elpwpw  4613  elpwuni  4616  rintn0  4619  dftr4  4757  uniixp  7931  fipwss  8335  dffi3  8337  uniwf  8682  numacn  8872  dfac12lem2  8966  fin23lem32  9166  isf34lem4  9199  isf34lem5  9200  fin1a2lem12  9233  itunitc1  9242  fpwwe2lem12  9463  tsksuc  9584  unirnioo  12273  restid  16094  mrcuni  16281  isacs3lem  17166  dmdprdd  18398  dprdfeq0  18421  dprdres  18427  dprdss  18428  dprdz  18429  subgdmdprd  18433  subgdprd  18434  dprd2dlem1  18440  dprd2da  18441  dmdprdsplit2lem  18444  ablfac1b  18469  lssintcl  18964  lbsextlem2  19159  lbsextlem3  19160  cssmre  20037  topgele  20734  topontopn  20744  unitg  20771  fctop  20808  cctop  20810  ppttop  20811  epttop  20813  mretopd  20896  toponmre  20897  resttopon  20965  ordtuni  20994  conncompcld  21237  islocfin  21320  kgentopon  21341  txuni2  21368  ptuni2  21379  ptbasfi  21384  xkouni  21402  prdstopn  21431  txdis  21435  txcmplem2  21445  xkococnlem  21462  qtoptop2  21502  qtopuni  21505  tgqtop  21515  opnfbas  21646  neifil  21684  filunibas  21685  trfil1  21690  flimfil  21773  cldsubg  21914  tgpconncompeqg  21915  tgpconncomp  21916  tsmsxplem1  21956  utoptop  22038  unirnblps  22224  unirnbl  22225  setsmstopn  22283  tngtopn  22454  bndth  22757  bcthlem5  23125  ovolficcss  23238  ovollb  23247  voliunlem2  23319  voliunlem3  23320  uniioovol  23347  uniioombl  23357  opnmbllem  23369  ubthlem1  27726  hsupcl  28198  hsupss  28200  hsupunss  28202  hsupval2  28268  unicls  29949  pwsiga  30193  sigainb  30199  insiga  30200  ddemeas  30299  omssubadd  30362  cvmsss2  31256  dfon2lem2  31689  ntruni  32322  clsint2  32324  neibastop1  32354  neibastop2lem  32355  neibastop3  32357  topmeet  32359  topjoin  32360  fnemeet1  32361  fnemeet2  32362  fnejoin1  32363  bj-intss  33053  opnmbllem0  33445  heiborlem1  33610  elrfi  37257  pwpwuni  39225  0ome  40743