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

Theorem sspwuni 4068
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 2867 . . . 4  |-  x  e. 
_V
21elpw 3707 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
32ralbii 2643 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
4 dfss3 3246 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
5 unissb 3938 . 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 1710   A.wral 2619    C_ wss 3228   ~Pcpw 3701   U.cuni 3908
This theorem is referenced by:  pwssb  4069  elpwuni  4070  rintn0  4073  dftr4  4199  uniixp  6927  fipwss  7272  dffi3  7274  uniwf  7581  numacn  7766  dfac12lem2  7860  fin23lem32  8060  isf34lem4  8093  isf34lem5  8094  fin1a2lem12  8127  itunitc1  8136  fpwwe2lem12  8353  tsksuc  8474  unirnioo  10835  restid  13437  mrcuni  13622  isacs3lem  14368  dmdprdd  15336  dprdfeq0  15356  dprdres  15362  dprdss  15363  dprdz  15364  subgdmdprd  15368  subgdprd  15369  dprd2dlem1  15375  dprd2da  15376  dmdprdsplit2lem  15379  ablfac1b  15404  lssintcl  15820  lbsextlem2  16011  lbsextlem3  16012  cssmre  16699  istps2OLD  16765  topgele  16778  topontopn  16786  fctop  16847  cctop  16849  ppttop  16850  epttop  16852  mretopd  16935  toponmre  16936  resttopon  16998  ordtuni  17026  concompcld  17266  kgentopon  17339  txuni2  17366  ptuni2  17377  ptbasfi  17382  xkouni  17400  prdstopn  17428  txdis  17432  txcmplem2  17442  xkococnlem  17459  qtoptop2  17496  qtopuni  17499  tgqtop  17509  opnfbas  17639  neifil  17677  filunibas  17678  trfil1  17683  flimfil  17766  cldsubg  17895  tgpconcompeqg  17896  tgpconcomp  17897  tsmsxplem1  17937  unirnbl  18071  setsmstopn  18126  tngtopn  18268  bndth  18560  bcthlem5  18854  ovolficcss  18933  ovollb  18942  voliunlem2  19012  voliunlem3  19013  uniioovol  19038  uniioombl  19048  opnmbllem  19060  ubthlem1  21563  hsupcl  22032  hsupss  22034  hsupunss  22036  hsupval2  22102  unicls  23457  utoptop  23538  pwsiga  23779  sigainb  23785  insiga  23786  cvmsss2  24209  dfon2lem2  24698  ntruni  25569  clsint2  25571  islocfin  25620  neibastop1  25632  neibastop2lem  25633  neibastop3  25635  topmeet  25637  topjoin  25638  fnemeet1  25639  fnemeet2  25640  fnejoin1  25641  heiborlem1  25858  elrfi  26092
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1546  ax-5 1557  ax-17 1616  ax-9 1654  ax-8 1675  ax-6 1729  ax-7 1734  ax-11 1746  ax-12 1930  ax-ext 2339
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1319  df-ex 1542  df-nf 1545  df-sb 1649  df-clab 2345  df-cleq 2351  df-clel 2354  df-nfc 2483  df-ral 2624  df-v 2866  df-in 3235  df-ss 3242  df-pw 3703  df-uni 3909
  Copyright terms: Public domain W3C validator