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

Theorem ssun1 3666
Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssun1

Proof of Theorem ssun1
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 orc 385 . . 3
2 elun 3644 . . 3
31, 2sylibr 212 . 2
43ssriv 3507 1
Colors of variables: wff setvar class
Syntax hints:  \/wo 368  e.wcel 1818  u.cun 3473  C_wss 3475
This theorem is referenced by:  ssun2  3667  ssun3  3668  elun1  3670  inabs  3728  reuun1  3779  un00  3862  snsspr1  4179  snsstp1  4181  snsstp2  4182  uniintsn  4324  sssucid  4960  sofld  5460  fvrn0  5893  ovima0  6454  unexb  6600  dmexg  6731  suppun  6939  dftpos2  6991  tpostpos2  6995  tfrlem11  7076  oaabs2  7313  ralxpmap  7488  domss2  7696  mapunen  7706  ac6sfi  7784  frfi  7785  unfir  7808  domunfican  7813  iunfi  7828  elfiun  7910  dffi3  7911  unwdomg  8031  unxpwdom2  8035  unxpwdom  8036  cantnfp1lem1  8118  cantnfp1lem3  8120  cantnfp1lem1OLD  8144  cantnfp1lem3OLD  8146  tc2  8194  unwf  8249  rankunb  8289  r0weon  8411  infxpenlem  8412  dfac2  8532  cdadom3  8589  cdainflem  8592  infunabs  8608  infcda  8609  infdif  8610  ackbij1lem15  8635  cfsmolem  8671  isfin4-3  8716  fin23lem11  8718  fin1a2lem10  8810  fin1a2lem13  8813  axdc3lem4  8854  axcclem  8858  zornn0g  8906  ttukeylem1  8910  ttukeylem5  8914  ttukeylem7  8916  fingch  9022  fpwwe2lem13  9041  gchac  9080  wunfi  9120  wundm  9127  wunex2  9137  inar1  9174  ressxr  9658  nnssnn0  10823  un0addcl  10854  un0mulcl  10855  hashbclem  12501  hashf1lem1  12504  hashf1lem2  12505  ccatfn  12591  ccatrn  12606  fsumsplit  13562  fsum2d  13586  fsumabs  13615  fsumrlim  13625  fsumo1  13626  incexclem  13648  fprodsplit  13770  fprod2d  13785  vdwapid1  14493  vdwlem6  14504  ramcl2  14534  isstruct2  14641  srngbase  14753  srngplusg  14754  srngmulr  14755  lmodbase  14762  lmodplusg  14763  lmodsca  14764  ipsbase  14769  ipsaddg  14770  ipsmulr  14771  phlbase  14779  phlplusg  14780  phlsca  14781  odrngbas  14805  odrngplusg  14806  odrngmulr  14807  prdssca  14853  prdsbas  14854  prdsplusg  14855  prdsmulr  14856  prdsvsca  14857  prdsip  14858  prdsle  14859  prdsds  14861  prdstset  14863  imasbas  14909  imasplusg  14914  imasmulr  14915  imassca  14916  imasvsca  14917  imasip  14918  mreexexlem2d  15042  drsdirfi  15567  ipobas  15785  ipotset  15787  acsfiindd  15807  psdmrn  15837  dirdm  15864  gsumzaddlemOLD  16936  gsumzsplit  16944  gsumzsplitOLD  16945  gsumsplit2  16948  gsumsplit2OLD  16949  gsumzunsnd  16982  gsum2dlem2  16998  gsum2dOLD  17000  dprdfadd  17060  dprdfaddOLD  17067  dmdprdsplit2lem  17094  dmdprdsplit2  17095  dmdprdsplit  17096  dprdsplit  17097  ablfac1eulem  17123  lspun  17633  lspsolv  17789  lsppratlem3  17795  islbs3  17801  lbsextlem2  17805  lbsextlem4  17807  psrbagaddcl  18020  psrbagaddclOLD  18021  psrbas  18030  psrbasOLD  18031  psrplusg  18034  psrmulr  18037  mplsubglem  18093  mplsubglemOLD  18095  mplcoe1  18127  mplcoe5  18131  mplcoe2OLD  18133  cnfldbas  18424  cnfldadd  18425  cnfldmul  18426  cnfldcj  18427  cnfldtset  18428  cnfldle  18429  cnfldds  18430  mdetunilem9  19122  basdif0  19454  ordtbas2  19692  ordtbas  19693  ordtopn1  19695  leordtval2  19713  iocpnfordt  19716  icomnfordt  19717  uncmp  19903  fiuncmp  19904  bwth  19910  locfincmp  20027  comppfsc  20033  1stckgenlem  20054  1stckgen  20055  ptbasin  20078  ptbasfi  20082  dfac14lem  20118  dfac14  20119  ptuncnv  20308  ptunhmeo  20309  ptcmpfi  20314  fbun  20341  trfil2  20388  ufprim  20410  ufileu  20420  filufint  20421  ufildr  20432  fmfnfm  20459  hausflim  20482  fclsfnflim  20528  alexsubALTlem4  20550  tmdgsum  20594  tsmsgsum  20637  tsmsgsumOLD  20640  tsmsresOLD  20645  tsmsres  20646  tsmssplit  20654  tsmsxplem1  20655  ustssco  20717  ustuqtop1  20744  prdsxmetlem  20871  prdsbl  20994  icccmplem2  21328  fsumcn  21374  cnmpt2pc  21428  rrxmetlem  21834  rrxmet  21835  rrxdstprj1  21836  ovolctb2  21903  ovolunnul  21911  ovolfiniun  21912  nulmbl2  21947  finiunmbl  21954  volfiniun  21957  icombl  21974  ioombl  21975  uniiccdif  21987  mbfres2  22052  itg2splitlem  22155  itg2split  22156  itgfsum  22233  itgsplit  22242  itgsplitioo  22244  dvreslem  22313  dvaddbr  22341  dvmulbr  22342  dvmptfsum  22376  lhop  22417  dvcnvrelem2  22419  mdegcl  22469  elplyr  22598  plyrem  22701  xrlimcnp  23298  fsumharmonic  23341  chtdif  23432  lgsdir2lem3  23600  lgsquadlem2  23630  dchrisum0lem1b  23700  pntrlog2bndlem6  23768  pntlemf  23790  ex-ss  25148  shsleji  26288  shsval2i  26305  ssjo  26365  sshhococi  26464  gsumle  27770  gsumvsca1  27773  gsumvsca2  27774  esumsplit  28063  aean  28216  sxbrsigalem2  28257  subfacp1lem2b  28625  subfacp1lem3  28626  subfacp1lem5  28628  kur14lem7  28656  kur14lem9  28658  cvmliftlem10  28739  dftrpred3g  29316  wfrlem14  29356  wfrlem15  29357  nofulllem4  29465  finixpnum  30038  mbfresfi  30061  refssfne  30176  filnetlem3  30198  prdsbnd  30289  heibor1lem  30305  rrnequiv  30331  elrfi  30626  mzpcompact2lem  30684  eldioph2  30695  eldioph4b  30745  ttac  30978  pwssplit4  31035  pwslnmlem2  31039  isnumbasgrplem2  31053  algbase  31127  algaddg  31128  algmulr  31129  fiuneneq  31154  idomsubgmo  31155  compne  31349  mccllem  31605  cncfiooicclem1  31696  dvmptfprod  31742  dvnprodlem1  31743  iblsplit  31765  fourierdlem54  31943  fourierdlem102  31991  fourierdlem103  31992  fourierdlem104  31993  fourierdlem114  32003  gsumsplit2f  32954  bnj931  33829  bj-unrab  34494  bj-snglsstag  34539  bj-2upln0  34581  bj-ccssccbar  34620  paddunssN  35532  sspadd1  35539  sspadd2  35540  pclfinN  35624  dochdmj1  37117  dvhdimlem  37171  trclubg  37785
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-or 370  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-v 3111  df-un 3480  df-in 3482  df-ss 3489
  Copyright terms: Public domain W3C validator