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

Theorem sspwuni 4411
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 4017 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
21ralbii 2895 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
3 dfss3 3494 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
4 unissb 4277 . 2  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
52, 3, 43bitr4i 277 1  |-  ( A 
C_  ~P B  <->  U. A  C_  B )
Colors of variables: wff setvar class
Syntax hints:    <-> wb 184    e. wcel 1767   A.wral 2814    C_ wss 3476   ~Pcpw 4010   U.cuni 4245
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-ral 2819  df-v 3115  df-in 3483  df-ss 3490  df-pw 4012  df-uni 4246
This theorem is referenced by:  pwssb  4412  elpwuni  4413  rintn0  4416  dftr4  4545  uniixp  7492  fipwss  7888  dffi3  7890  uniwf  8236  numacn  8429  dfac12lem2  8523  fin23lem32  8723  isf34lem4  8756  isf34lem5  8757  fin1a2lem12  8790  itunitc1  8799  fpwwe2lem12  9018  tsksuc  9139  unirnioo  11623  restid  14688  mrcuni  14875  isacs3lem  15652  dmdprdd  16830  dprdfeq0  16861  dprdfeq0OLD  16868  dprdres  16874  dprdss  16875  dprdz  16876  subgdmdprd  16880  subgdprd  16881  dprd2dlem1  16889  dprd2da  16890  dmdprdsplit2lem  16893  ablfac1b  16920  lssintcl  17405  lbsextlem2  17600  lbsextlem3  17601  cssmre  18507  istps2OLD  19205  topgele  19218  topontopn  19226  fctop  19287  cctop  19289  ppttop  19290  epttop  19292  mretopd  19375  toponmre  19376  resttopon  19444  ordtuni  19473  concompcld  19717  kgentopon  19790  txuni2  19817  ptuni2  19828  ptbasfi  19833  xkouni  19851  prdstopn  19880  txdis  19884  txcmplem2  19894  xkococnlem  19911  qtoptop2  19951  qtopuni  19954  tgqtop  19964  opnfbas  20094  neifil  20132  filunibas  20133  trfil1  20138  flimfil  20221  cldsubg  20360  tgpconcompeqg  20361  tgpconcomp  20362  tsmsxplem1  20406  utoptop  20488  unirnblps  20673  unirnbl  20674  setsmstopn  20732  tngtopn  20915  bndth  21209  bcthlem5  21518  ovolficcss  21632  ovollb  21641  voliunlem2  21712  voliunlem3  21713  uniioovol  21739  uniioombl  21749  opnmbllem  21761  ubthlem1  25478  hsupcl  25949  hsupss  25951  hsupunss  25953  hsupval2  26019  unicls  27537  pwsiga  27786  sigainb  27792  insiga  27793  ddemeas  27864  cvmsss2  28375  dfon2lem2  28809  opnmbllem0  29643  ntruni  29738  clsint2  29740  islocfin  29784  neibastop1  29796  neibastop2lem  29797  neibastop3  29799  topmeet  29801  topjoin  29802  fnemeet1  29803  fnemeet2  29804  fnejoin1  29805  heiborlem1  29926  elrfi  30246
  Copyright terms: Public domain W3C validator