MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspwuni Structured version   Unicode version

Theorem sspwuni 4391
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.
StepHypRef Expression
1 selpw 3992 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
21ralbii 2863 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
3 dfss3 3460 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
4 unissb 4253 . 2  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
52, 3, 43bitr4i 280 1  |-  ( A 
C_  ~P B  <->  U. A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 187    e. wcel 1870   A.wral 2782    C_ wss 3442   ~Pcpw 3985   U.cuni 4222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-ral 2787  df-v 3089  df-in 3449  df-ss 3456  df-pw 3987  df-uni 4223
This theorem is referenced by:  pwssb  4392  elpwuni  4393  rintn0  4396  dftr4  4525  uniixp  7553  fipwss  7949  dffi3  7951  uniwf  8289  numacn  8478  dfac12lem2  8572  fin23lem32  8772  isf34lem4  8805  isf34lem5  8806  fin1a2lem12  8839  itunitc1  8848  fpwwe2lem12  9065  tsksuc  9186  unirnioo  11734  restid  15291  mrcuni  15478  isacs3lem  16363  dmdprdd  17566  dprdfeq0  17590  dprdres  17596  dprdss  17597  dprdz  17598  subgdmdprd  17602  subgdprd  17603  dprd2dlem1  17609  dprd2da  17610  dmdprdsplit2lem  17613  ablfac1b  17638  lssintcl  18122  lbsextlem2  18317  lbsextlem3  18318  cssmre  19187  topgele  19880  topontopn  19888  unitg  19913  fctop  19950  cctop  19952  ppttop  19953  epttop  19955  mretopd  20039  toponmre  20040  resttopon  20108  ordtuni  20137  concompcld  20380  islocfin  20463  kgentopon  20484  txuni2  20511  ptuni2  20522  ptbasfi  20527  xkouni  20545  prdstopn  20574  txdis  20578  txcmplem2  20588  xkococnlem  20605  qtoptop2  20645  qtopuni  20648  tgqtop  20658  opnfbas  20788  neifil  20826  filunibas  20827  trfil1  20832  flimfil  20915  cldsubg  21056  tgpconcompeqg  21057  tgpconcomp  21058  tsmsxplem1  21098  utoptop  21180  unirnblps  21365  unirnbl  21366  setsmstopn  21424  tngtopn  21589  bndth  21882  bcthlem5  22189  ovolficcss  22301  ovollb  22310  voliunlem2  22381  voliunlem3  22382  uniioovol  22413  uniioombl  22424  opnmbllem  22436  ubthlem1  26357  hsupcl  26827  hsupss  26829  hsupunss  26831  hsupval2  26897  unicls  28548  pwsiga  28791  sigainb  28797  insiga  28798  ddemeas  28898  omssubadd  28961  cvmsss2  29785  dfon2lem2  30217  ntruni  30768  clsint2  30770  neibastop1  30800  neibastop2lem  30801  neibastop3  30803  topmeet  30805  topjoin  30806  fnemeet1  30807  fnemeet2  30808  fnejoin1  30809  opnmbllem0  31679  heiborlem1  31846  elrfi  35244  pwpwuni  37037
  Copyright terms: Public domain W3C validator