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

Theorem sspwuni 4251
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 3862 . . 3  |-  ( x  e.  ~P B  <->  x  C_  B
)
21ralbii 2734 . 2  |-  ( A. x  e.  A  x  e.  ~P B  <->  A. x  e.  A  x  C_  B
)
3 dfss3 3341 . 2  |-  ( A 
C_  ~P B  <->  A. x  e.  A  x  e.  ~P B )
4 unissb 4118 . 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 1756   A.wral 2710    C_ wss 3323   ~Pcpw 3855   U.cuni 4086
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-ral 2715  df-v 2969  df-in 3330  df-ss 3337  df-pw 3857  df-uni 4087
This theorem is referenced by:  pwssb  4252  elpwuni  4253  rintn0  4256  dftr4  4385  uniixp  7278  fipwss  7671  dffi3  7673  uniwf  8018  numacn  8211  dfac12lem2  8305  fin23lem32  8505  isf34lem4  8538  isf34lem5  8539  fin1a2lem12  8572  itunitc1  8581  fpwwe2lem12  8800  tsksuc  8921  unirnioo  11381  restid  14364  mrcuni  14551  isacs3lem  15328  dmdprdd  16469  dprdfeq0  16500  dprdfeq0OLD  16507  dprdres  16513  dprdss  16514  dprdz  16515  subgdmdprd  16519  subgdprd  16520  dprd2dlem1  16528  dprd2da  16529  dmdprdsplit2lem  16532  ablfac1b  16559  lssintcl  17022  lbsextlem2  17217  lbsextlem3  17218  cssmre  18093  istps2OLD  18501  topgele  18514  topontopn  18522  fctop  18583  cctop  18585  ppttop  18586  epttop  18588  mretopd  18671  toponmre  18672  resttopon  18740  ordtuni  18769  concompcld  19013  kgentopon  19086  txuni2  19113  ptuni2  19124  ptbasfi  19129  xkouni  19147  prdstopn  19176  txdis  19180  txcmplem2  19190  xkococnlem  19207  qtoptop2  19247  qtopuni  19250  tgqtop  19260  opnfbas  19390  neifil  19428  filunibas  19429  trfil1  19434  flimfil  19517  cldsubg  19656  tgpconcompeqg  19657  tgpconcomp  19658  tsmsxplem1  19702  utoptop  19784  unirnblps  19969  unirnbl  19970  setsmstopn  20028  tngtopn  20211  bndth  20505  bcthlem5  20814  ovolficcss  20928  ovollb  20937  voliunlem2  21007  voliunlem3  21008  uniioovol  21034  uniioombl  21044  opnmbllem  21056  ubthlem1  24222  hsupcl  24693  hsupss  24695  hsupunss  24697  hsupval2  24763  unicls  26285  pwsiga  26525  sigainb  26531  insiga  26532  ddemeas  26604  cvmsss2  27115  dfon2lem2  27548  opnmbllem0  28380  ntruni  28475  clsint2  28477  islocfin  28521  neibastop1  28533  neibastop2lem  28534  neibastop3  28536  topmeet  28538  topjoin  28539  fnemeet1  28540  fnemeet2  28541  fnejoin1  28542  heiborlem1  28663  elrfi  28983
  Copyright terms: Public domain W3C validator