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

Theorem ssun1 3339
Description: Subclass relationship for union of classes. Theorem 25 of [Suppes] p. 27. (Contributed by NM, 5-Aug-1993.)
Assertion
Ref Expression
ssun1  |-  A  C_  ( A  u.  B
)
Dummy variable  x is distinct from all other variables.

Proof of Theorem ssun1
StepHypRef Expression
1 orc 376 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3317 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 205 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3185 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    e. wcel 1685    u. cun 3151    C_ wss 3153
This theorem is referenced by:  ssun2  3340  ssun3  3341  elun1  3343  inabs  3401  reuun1  3451  un00  3491  snsspr1  3765  snsstp1  3767  snsstp2  3768  uniintsn  3900  sssucid  4468  unexb  4519  dmexg  4938  sofld  5120  fvrn0  5511  dftpos2  6212  tpostpos2  6216  riotassuni  6338  tfrlem11  6399  oaabs2  6638  ersym  6667  domss2  7015  mapunen  7025  ac6sfi  7096  frfi  7097  unfir  7120  domunfican  7124  iunfi  7139  finsschain  7157  elfiun  7178  dffi3  7179  unwdomg  7293  unxpwdom2  7297  unxpwdom  7298  cantnfp1lem1  7375  cantnfp1lem3  7377  tc2  7422  unwf  7477  rankunb  7517  r0weon  7635  infxpenlem  7636  dfac2  7752  cdadom3  7809  cdainflem  7812  infunabs  7828  infcda  7829  infdif  7830  ackbij1lem15  7855  ackbij1lem16  7856  cfsmolem  7891  isfin4-3  7936  fin23lem11  7938  fin1a2lem10  8030  fin1a2lem13  8033  axdc3lem4  8074  axcclem  8078  zornn0g  8127  ttukeylem1  8131  ttukeylem5  8135  ttukeylem7  8137  fingch  8240  fpwwe2lem13  8259  gchac  8290  wunfi  8338  wundm  8345  wunex2  8355  inar1  8392  ressxr  8871  nnssnn0  9963  un0addcl  9992  un0mulcl  9993  hashbclem  11384  hashf1lem1  11387  hashf1lem2  11388  ccatfn  11421  fsumsplit  12206  sumsplit  12225  fsum2d  12228  fsumabs  12253  fsumrlim  12263  fsumo1  12264  fsumiun  12273  incexclem  12289  vdwapid1  13016  vdwlem6  13027  ramcl2  13057  isstruct2  13151  srngbase  13258  srngplusg  13259  srngmulr  13260  lmodbase  13267  lmodplusg  13268  lmodsca  13269  algbase  13272  algaddg  13273  algmulr  13274  phlbase  13282  phlplusg  13283  phlsca  13284  odrngbas  13306  odrngplusg  13307  odrngmulr  13308  prdssca  13350  prdsbas  13351  prdsplusg  13352  prdsmulr  13353  prdsvsca  13354  prdsle  13355  prdsds  13357  prdstset  13359  imasbas  13409  imasplusg  13414  imasmulr  13415  imassca  13416  imasvsca  13417  mreexexlem2d  13541  yonedalem1  14040  yonedalem21  14041  yonedalem22  14046  yonffthlem  14050  drsdirfi  14066  ipobas  14252  ipotset  14254  acsfiindd  14274  psdmrn  14310  dirdm  14350  gsumzaddlem  15197  gsumzsplit  15200  gsumsplit2  15202  gsum2d  15217  dprdfadd  15249  dmdprdsplit2lem  15274  dmdprdsplit2  15275  dmdprdsplit  15276  dprdsplit  15277  ablfac1eulem  15301  lspun  15738  lsmsp  15833  lspsolv  15890  lsppratlem3  15896  islbs3  15902  lbsextlem2  15906  lbsextlem4  15908  psrbagaddcl  16110  psrbas  16118  psrplusg  16120  psrmulr  16123  mplsubglem  16173  mplcoe1  16203  mplcoe2  16205  cnfldbas  16377  cnfldadd  16378  cnfldmul  16379  cnfldcj  16380  basdif0  16685  tgdif0  16724  ordtbas2  16915  ordtbas  16916  ordtopn1  16918  leordtval2  16936  iocpnfordt  16939  icomnfordt  16940  uncmp  17124  fiuncmp  17125  1stckgenlem  17242  1stckgen  17243  ptbasin  17266  ptbasfi  17270  dfac14lem  17305  dfac14  17306  ptuncnv  17492  ptunhmeo  17493  ptcmpfi  17498  fbun  17529  trfil2  17576  isufil2  17597  ufprim  17598  ufileu  17608  filufint  17609  ufildr  17620  fmfnfm  17647  hausflim  17670  flimclslem  17673  fclsfnflim  17716  flimfnfcls  17717  alexsubALTlem4  17738  tmdgsum  17772  tsmsgsum  17815  tsmsres  17820  tsmssplit  17828  tsmsxplem1  17829  prdsxmetlem  17926  imasdsf1olem  17931  prdsbl  18031  icccmplem2  18322  fsumcn  18368  cnmpt2pc  18420  iccpnfcnv  18436  ovolctb2  18845  ovolunnul  18853  ovolfiniun  18854  nulmbl2  18888  finiunmbl  18895  volfiniun  18898  icombl  18915  ioombl  18916  uniiccdif  18927  mbfres2  18994  itg2splitlem  19097  itg2split  19098  itgfsum  19175  itgsplit  19184  itgsplitioo  19186  limcdif  19220  dvreslem  19253  dvaddbr  19281  dvmulbr  19282  dvmptfsum  19316  lhop  19357  dvcnvrelem2  19359  mdegcl  19449  elplyr  19577  plyrem  19679  xrlimcnp  20257  jensenlem1  20275  jensenlem2  20276  jensen  20277  fsumharmonic  20299  chtdif  20390  lgsdir2lem3  20558  lgsquadlem2  20588  dchrisum0lem1b  20658  pntrlog2bndlem6  20726  pntlemf  20748  ex-ss  20789  shsleji  21941  shsval2i  21958  ssjo  22018  sshhococi  22117  subfacp1lem2b  23116  subfacp1lem3  23117  subfacp1lem5  23119  kur14lem7  23147  kur14lem9  23149  cvmliftlem10  23229  dftrpred3g  23637  wfrlem14  23670  wfrlem15  23671  axfelem13  23759  domfldrefc  24455  prl  24566  basexre  24921  islimrs4  24981  segray  25554  refssfne  25693  locfincmp  25703  comppfsc  25706  filnetlem3  25728  prdsbnd  25916  heibor1lem  25932  rrnequiv  25958  ralxpmap  26160  elrfi  26168  mzpcompact2lem  26228  eldioph2  26240  eldioph4b  26293  ttac  26528  pwssplit4  26590  pwslnmlem2  26594  isnumbasgrplem2  26668  rngunsnply  26777  fiuneneq  26912  idomsubgmo  26913  compne  27041  bnj931  28069  paddunssN  29264  sspadd1  29271  sspadd2  29272  pclfinN  29356  dochdmj1  30847  dvhdimlem  30901
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-un 3158  df-in 3160  df-ss 3167
  Copyright terms: Public domain W3C validator