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

Theorem sspwuni 4176
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 vex 2959 . . . 4  |-  x  e. 
_V
21elpw 3805 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
32ralbii 2729 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
4 dfss3 3338 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
5 unissb 4045 . 2  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
63, 4, 53bitr4i 269 1  |-  ( A 
C_  ~P B  <->  U. A  C_  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 177    e. wcel 1725   A.wral 2705    C_ wss 3320   ~Pcpw 3799   U.cuni 4015
This theorem is referenced by:  pwssb  4177  elpwuni  4178  rintn0  4181  dftr4  4307  uniixp  7085  fipwss  7434  dffi3  7436  uniwf  7745  numacn  7930  dfac12lem2  8024  fin23lem32  8224  isf34lem4  8257  isf34lem5  8258  fin1a2lem12  8291  itunitc1  8300  fpwwe2lem12  8516  tsksuc  8637  unirnioo  11004  restid  13661  mrcuni  13846  isacs3lem  14592  dmdprdd  15560  dprdfeq0  15580  dprdres  15586  dprdss  15587  dprdz  15588  subgdmdprd  15592  subgdprd  15593  dprd2dlem1  15599  dprd2da  15600  dmdprdsplit2lem  15603  ablfac1b  15628  lssintcl  16040  lbsextlem2  16231  lbsextlem3  16232  cssmre  16920  istps2OLD  16986  topgele  16999  topontopn  17007  fctop  17068  cctop  17070  ppttop  17071  epttop  17073  mretopd  17156  toponmre  17157  resttopon  17225  ordtuni  17254  concompcld  17497  kgentopon  17570  txuni2  17597  ptuni2  17608  ptbasfi  17613  xkouni  17631  prdstopn  17660  txdis  17664  txcmplem2  17674  xkococnlem  17691  qtoptop2  17731  qtopuni  17734  tgqtop  17744  opnfbas  17874  neifil  17912  filunibas  17913  trfil1  17918  flimfil  18001  cldsubg  18140  tgpconcompeqg  18141  tgpconcomp  18142  tsmsxplem1  18182  utoptop  18264  unirnblps  18449  unirnbl  18450  setsmstopn  18508  tngtopn  18691  bndth  18983  bcthlem5  19281  ovolficcss  19366  ovollb  19375  voliunlem2  19445  voliunlem3  19446  uniioovol  19471  uniioombl  19481  opnmbllem  19493  ubthlem1  22372  hsupcl  22841  hsupss  22843  hsupunss  22845  hsupval2  22911  unicls  24301  pwsiga  24513  sigainb  24519  insiga  24520  cvmsss2  24961  dfon2lem2  25411  opnmbllem0  26242  ntruni  26330  clsint2  26332  islocfin  26376  neibastop1  26388  neibastop2lem  26389  neibastop3  26391  topmeet  26393  topjoin  26394  fnemeet1  26395  fnemeet2  26396  fnejoin1  26397  heiborlem1  26520  elrfi  26748
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-ral 2710  df-v 2958  df-in 3327  df-ss 3334  df-pw 3801  df-uni 4016
  Copyright terms: Public domain W3C validator