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

Theorem sspwuni 3987
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 2791 . . . 4  |-  x  e. 
_V
21elpw 3631 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
32ralbii 2567 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
4 dfss3 3170 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
5 unissb 3857 . 2  |-  ( U. A  C_  B  <->  A. x  e.  A  x  C_  B
)
63, 4, 53bitr4i 268 1  |-  ( A 
C_  ~P B  <->  U. A  C_  B )
Colors of variables: wff set class
Syntax hints:    <-> wb 176    e. wcel 1684   A.wral 2543    C_ wss 3152   ~Pcpw 3625   U.cuni 3827
This theorem is referenced by:  pwssb  3988  elpwuni  3989  rintn0  3992  dftr4  4118  uniixp  6839  fipwss  7182  dffi3  7184  uniwf  7491  numacn  7676  dfac12lem2  7770  fin23lem32  7970  isf34lem4  8003  isf34lem5  8004  fin1a2lem12  8037  itunitc1  8046  fpwwe2lem12  8263  tsksuc  8384  unirnioo  10743  restid  13338  mrcuni  13523  isacs3lem  14269  dmdprdd  15237  dprdfeq0  15257  dprdres  15263  dprdss  15264  dprdz  15265  subgdmdprd  15269  subgdprd  15270  dprd2dlem1  15276  dprd2da  15277  dmdprdsplit2lem  15280  ablfac1b  15305  lssintcl  15721  lbsextlem2  15912  lbsextlem3  15913  cssmre  16593  istps2OLD  16659  topgele  16672  topontopn  16680  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  mretopd  16829  toponmre  16830  resttopon  16892  ordtuni  16920  concompcld  17160  kgentopon  17233  txuni2  17260  ptuni2  17271  ptbasfi  17276  xkouni  17294  prdstopn  17322  txdis  17326  txcmplem2  17336  xkococnlem  17353  qtoptop2  17390  qtopuni  17393  tgqtop  17403  opnfbas  17537  neifil  17575  filunibas  17576  trfil1  17581  flimfil  17664  cldsubg  17793  tgpconcompeqg  17794  tgpconcomp  17795  tsmsxplem1  17835  unirnbl  17969  setsmstopn  18024  tngtopn  18166  bndth  18456  bcthlem5  18750  ovolficcss  18829  ovollb  18838  voliunlem2  18908  voliunlem3  18909  uniioovol  18934  uniioombl  18944  opnmbllem  18956  ubthlem1  21449  hsupcl  21918  hsupss  21920  hsupunss  21922  hsupval2  21988  clduni  23289  pwsiga  23491  sigainb  23497  insiga  23498  cvmsss2  23805  dfon2lem2  24140  ump  25046  ntruni  26245  clsint2  26247  islocfin  26296  neibastop1  26308  neibastop2lem  26309  neibastop3  26311  topmeet  26313  topjoin  26314  fnemeet1  26315  fnemeet2  26316  fnejoin1  26317  heiborlem1  26535  elrfi  26769
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ral 2548  df-v 2790  df-in 3159  df-ss 3166  df-pw 3627  df-uni 3828
  Copyright terms: Public domain W3C validator