MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  sspwuni Structured 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 3978 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
21ralbii 2839 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
3 dfss3 3457 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
4 unissb 4234 . 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 1758   A.wral 2799    C_ wss 3439   ~Pcpw 3971   U.cuni 4202
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-ral 2804  df-v 3080  df-in 3446  df-ss 3453  df-pw 3973  df-uni 4203
This theorem is referenced by:  pwssb  4368  elpwuni  4369  rintn0  4372  dftr4  4501  uniixp  7399  fipwss  7793  dffi3  7795  uniwf  8140  numacn  8333  dfac12lem2  8427  fin23lem32  8627  isf34lem4  8660  isf34lem5  8661  fin1a2lem12  8694  itunitc1  8703  fpwwe2lem12  8922  tsksuc  9043  unirnioo  11509  restid  14494  mrcuni  14681  isacs3lem  15458  dmdprdd  16606  dprdfeq0  16637  dprdfeq0OLD  16644  dprdres  16650  dprdss  16651  dprdz  16652  subgdmdprd  16656  subgdprd  16657  dprd2dlem1  16665  dprd2da  16666  dmdprdsplit2lem  16669  ablfac1b  16696  lssintcl  17171  lbsextlem2  17366  lbsextlem3  17367  cssmre  18246  istps2OLD  18661  topgele  18674  topontopn  18682  fctop  18743  cctop  18745  ppttop  18746  epttop  18748  mretopd  18831  toponmre  18832  resttopon  18900  ordtuni  18929  concompcld  19173  kgentopon  19246  txuni2  19273  ptuni2  19284  ptbasfi  19289  xkouni  19307  prdstopn  19336  txdis  19340  txcmplem2  19350  xkococnlem  19367  qtoptop2  19407  qtopuni  19410  tgqtop  19420  opnfbas  19550  neifil  19588  filunibas  19589  trfil1  19594  flimfil  19677  cldsubg  19816  tgpconcompeqg  19817  tgpconcomp  19818  tsmsxplem1  19862  utoptop  19944  unirnblps  20129  unirnbl  20130  setsmstopn  20188  tngtopn  20371  bndth  20665  bcthlem5  20974  ovolficcss  21088  ovollb  21097  voliunlem2  21168  voliunlem3  21169  uniioovol  21195  uniioombl  21205  opnmbllem  21217  ubthlem1  24443  hsupcl  24914  hsupss  24916  hsupunss  24918  hsupval2  24984  unicls  26498  pwsiga  26738  sigainb  26744  insiga  26745  ddemeas  26816  cvmsss2  27327  dfon2lem2  27761  opnmbllem0  28595  ntruni  28690  clsint2  28692  islocfin  28736  neibastop1  28748  neibastop2lem  28749  neibastop3  28751  topmeet  28753  topjoin  28754  fnemeet1  28755  fnemeet2  28756  fnejoin1  28757  heiborlem1  28878  elrfi  29198
  Copyright terms: Public domain W3C validator