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

Theorem sspwuni 4136
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 2919 . . . 4  |-  x  e. 
_V
21elpw 3765 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
32ralbii 2690 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
4 dfss3 3298 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
5 unissb 4005 . 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 1721   A.wral 2666    C_ wss 3280   ~Pcpw 3759   U.cuni 3975
This theorem is referenced by:  pwssb  4137  elpwuni  4138  rintn0  4141  dftr4  4267  uniixp  7044  fipwss  7392  dffi3  7394  uniwf  7701  numacn  7886  dfac12lem2  7980  fin23lem32  8180  isf34lem4  8213  isf34lem5  8214  fin1a2lem12  8247  itunitc1  8256  fpwwe2lem12  8472  tsksuc  8593  unirnioo  10960  restid  13616  mrcuni  13801  isacs3lem  14547  dmdprdd  15515  dprdfeq0  15535  dprdres  15541  dprdss  15542  dprdz  15543  subgdmdprd  15547  subgdprd  15548  dprd2dlem1  15554  dprd2da  15555  dmdprdsplit2lem  15558  ablfac1b  15583  lssintcl  15995  lbsextlem2  16186  lbsextlem3  16187  cssmre  16875  istps2OLD  16941  topgele  16954  topontopn  16962  fctop  17023  cctop  17025  ppttop  17026  epttop  17028  mretopd  17111  toponmre  17112  resttopon  17179  ordtuni  17208  concompcld  17450  kgentopon  17523  txuni2  17550  ptuni2  17561  ptbasfi  17566  xkouni  17584  prdstopn  17613  txdis  17617  txcmplem2  17627  xkococnlem  17644  qtoptop2  17684  qtopuni  17687  tgqtop  17697  opnfbas  17827  neifil  17865  filunibas  17866  trfil1  17871  flimfil  17954  cldsubg  18093  tgpconcompeqg  18094  tgpconcomp  18095  tsmsxplem1  18135  utoptop  18217  unirnblps  18402  unirnbl  18403  setsmstopn  18461  tngtopn  18644  bndth  18936  bcthlem5  19234  ovolficcss  19319  ovollb  19328  voliunlem2  19398  voliunlem3  19399  uniioovol  19424  uniioombl  19434  opnmbllem  19446  ubthlem1  22325  hsupcl  22794  hsupss  22796  hsupunss  22798  hsupval2  22864  unicls  24254  pwsiga  24466  sigainb  24472  insiga  24473  cvmsss2  24914  dfon2lem2  25354  ntruni  26220  clsint2  26222  islocfin  26266  neibastop1  26278  neibastop2lem  26279  neibastop3  26281  topmeet  26283  topjoin  26284  fnemeet1  26285  fnemeet2  26286  fnejoin1  26287  heiborlem1  26410  elrfi  26638
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-ral 2671  df-v 2918  df-in 3287  df-ss 3294  df-pw 3761  df-uni 3976
  Copyright terms: Public domain W3C validator