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

Theorem sspwuni 4367
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 3958 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
21ralbii 2819 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
3 dfss3 3422 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
4 unissb 4229 . 2  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
52, 3, 43bitr4i 281 1  |-  ( A 
C_  ~P B  <->  U. A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 188    e. wcel 1887   A.wral 2737    C_ wss 3404   ~Pcpw 3951   U.cuni 4198
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-ral 2742  df-v 3047  df-in 3411  df-ss 3418  df-pw 3953  df-uni 4199
This theorem is referenced by:  pwssb  4368  elpwuni  4369  rintn0  4372  dftr4  4502  uniixp  7545  fipwss  7943  dffi3  7945  uniwf  8290  numacn  8480  dfac12lem2  8574  fin23lem32  8774  isf34lem4  8807  isf34lem5  8808  fin1a2lem12  8841  itunitc1  8850  fpwwe2lem12  9066  tsksuc  9187  unirnioo  11734  restid  15332  mrcuni  15527  isacs3lem  16412  dmdprdd  17631  dprdfeq0  17655  dprdres  17661  dprdss  17662  dprdz  17663  subgdmdprd  17667  subgdprd  17668  dprd2dlem1  17674  dprd2da  17675  dmdprdsplit2lem  17678  ablfac1b  17703  lssintcl  18187  lbsextlem2  18382  lbsextlem3  18383  cssmre  19256  topgele  19949  topontopn  19957  unitg  19982  fctop  20019  cctop  20021  ppttop  20022  epttop  20024  mretopd  20108  toponmre  20109  resttopon  20177  ordtuni  20206  concompcld  20449  islocfin  20532  kgentopon  20553  txuni2  20580  ptuni2  20591  ptbasfi  20596  xkouni  20614  prdstopn  20643  txdis  20647  txcmplem2  20657  xkococnlem  20674  qtoptop2  20714  qtopuni  20717  tgqtop  20727  opnfbas  20857  neifil  20895  filunibas  20896  trfil1  20901  flimfil  20984  cldsubg  21125  tgpconcompeqg  21126  tgpconcomp  21127  tsmsxplem1  21167  utoptop  21249  unirnblps  21434  unirnbl  21435  setsmstopn  21493  tngtopn  21658  bndth  21986  bcthlem5  22296  ovolficcss  22422  ovollb  22432  voliunlem2  22504  voliunlem3  22505  uniioovol  22536  uniioombl  22547  opnmbllem  22559  ubthlem1  26512  hsupcl  26992  hsupss  26994  hsupunss  26996  hsupval2  27062  unicls  28709  pwsiga  28952  sigainb  28958  insiga  28959  ddemeas  29059  omssubadd  29128  omssubaddOLD  29132  cvmsss2  29997  dfon2lem2  30430  ntruni  30983  clsint2  30985  neibastop1  31015  neibastop2lem  31016  neibastop3  31018  topmeet  31020  topjoin  31021  fnemeet1  31022  fnemeet2  31023  fnejoin1  31024  opnmbllem0  31976  heiborlem1  32143  elrfi  35536  pwpwuni  37397  0ome  38350
  Copyright terms: Public domain W3C validator