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

Theorem sspwuni 4416
Description: Subclass relationship for power class and union. (Contributed by NM, 18-Jul-2006.)
Assertion
Ref Expression
sspwuni

Proof of Theorem sspwuni
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 selpw 4019 . . 3
21ralbii 2888 . 2
3 dfss3 3493 . 2
4 unissb 4281 . 2
52, 3, 43bitr4i 277 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  e.wcel 1818  A.wral 2807  C_wss 3475  ~Pcpw 4012  U.cuni 4249
This theorem is referenced by:  pwssb  4417  elpwuni  4418  rintn0  4421  dftr4  4550  uniixp  7512  fipwss  7909  dffi3  7911  uniwf  8258  numacn  8451  dfac12lem2  8545  fin23lem32  8745  isf34lem4  8778  isf34lem5  8779  fin1a2lem12  8812  itunitc1  8821  fpwwe2lem12  9040  tsksuc  9161  unirnioo  11653  restid  14831  mrcuni  15018  isacs3lem  15796  dmdprdd  17030  dprdfeq0  17062  dprdfeq0OLD  17069  dprdres  17075  dprdss  17076  dprdz  17077  subgdmdprd  17081  subgdprd  17082  dprd2dlem1  17090  dprd2da  17091  dmdprdsplit2lem  17094  ablfac1b  17121  lssintcl  17610  lbsextlem2  17805  lbsextlem3  17806  cssmre  18724  istps2OLD  19422  topgele  19435  topontopn  19443  unitg  19468  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  mretopd  19593  toponmre  19594  resttopon  19662  ordtuni  19691  concompcld  19935  islocfin  20018  kgentopon  20039  txuni2  20066  ptuni2  20077  ptbasfi  20082  xkouni  20100  prdstopn  20129  txdis  20133  txcmplem2  20143  xkococnlem  20160  qtoptop2  20200  qtopuni  20203  tgqtop  20213  opnfbas  20343  neifil  20381  filunibas  20382  trfil1  20387  flimfil  20470  cldsubg  20609  tgpconcompeqg  20610  tgpconcomp  20611  tsmsxplem1  20655  utoptop  20737  unirnblps  20922  unirnbl  20923  setsmstopn  20981  tngtopn  21164  bndth  21458  bcthlem5  21767  ovolficcss  21881  ovollb  21890  voliunlem2  21961  voliunlem3  21962  uniioovol  21988  uniioombl  21998  opnmbllem  22010  ubthlem1  25786  hsupcl  26257  hsupss  26259  hsupunss  26261  hsupval2  26327  unicls  27885  pwsiga  28130  sigainb  28136  insiga  28137  ddemeas  28208  cvmsss2  28719  dfon2lem2  29216  opnmbllem0  30050  ntruni  30145  clsint2  30147  neibastop1  30177  neibastop2lem  30178  neibastop3  30180  topmeet  30182  topjoin  30183  fnemeet1  30184  fnemeet2  30185  fnejoin1  30186  heiborlem1  30307  elrfi  30626
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-ral 2812  df-v 3111  df-in 3482  df-ss 3489  df-pw 4014  df-uni 4250
  Copyright terms: Public domain W3C validator