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

Theorem ssun1 3609
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
)

Proof of Theorem ssun1
Dummy variable  x is distinct from all other variables.
StepHypRef Expression
1 orc 391 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3586 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 217 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3448 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 374    e. wcel 1898    u. cun 3414    C_ wss 3416
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1680  ax-4 1693  ax-5 1769  ax-6 1816  ax-7 1862  ax-10 1926  ax-11 1931  ax-12 1944  ax-13 2102  ax-ext 2442
This theorem depends on definitions:  df-bi 190  df-or 376  df-an 377  df-tru 1458  df-ex 1675  df-nf 1679  df-sb 1809  df-clab 2449  df-cleq 2455  df-clel 2458  df-nfc 2592  df-v 3059  df-un 3421  df-in 3423  df-ss 3430
This theorem is referenced by:  ssun2  3610  ssun3  3611  elun1  3613  inabs  3686  reuun1  3737  un00  3812  snsspr1  4134  snsstp1  4136  snsstp2  4137  uniintsn  4286  sofld  5303  sssucid  5519  fvrn0  5910  ovima0  6475  unexb  6618  dmexg  6751  suppun  6962  dftpos2  7016  tpostpos2  7020  wfrlem14  7075  wfrlem15  7076  tfrlem11  7132  oaabs2  7372  ralxpmap  7547  domss2  7757  mapunen  7767  ac6sfi  7841  frfi  7842  unfir  7865  domunfican  7870  iunfi  7888  elfiun  7970  dffi3  7971  unwdomg  8125  unxpwdom2  8129  unxpwdom  8130  cantnfp1lem1  8209  cantnfp1lem3  8211  tc2  8252  unwf  8307  rankunb  8347  r0weon  8469  infxpenlem  8470  dfac2  8587  cdadom3  8644  cdainflem  8647  infunabs  8663  infcda  8664  infdif  8665  ackbij1lem15  8690  cfsmolem  8726  isfin4-3  8771  fin23lem11  8773  fin1a2lem10  8865  fin1a2lem13  8868  axdc3lem4  8909  axcclem  8913  zornn0g  8961  ttukeylem1  8965  ttukeylem5  8969  ttukeylem7  8971  fingch  9074  fpwwe2lem13  9093  gchac  9132  wunfi  9172  wundm  9179  wunex2  9189  inar1  9226  ressxr  9710  nnssnn0  10901  un0addcl  10932  un0mulcl  10933  hashbclem  12648  hashf1lem1  12651  hashf1lem2  12652  ccatfnOLD  12754  ccatrn  12769  trclublem  13108  relexpdmg  13154  relexpaddg  13165  fsumsplit  13855  fsum2d  13881  fsumabs  13910  fsumrlim  13920  fsumo1  13921  incexclem  13943  fprodsplit  14069  fprod2d  14084  lcmfunsnlem1  14659  coprmprod  14727  vdwapid1  14974  vdwlem6  14985  ramcl2  15022  ramcl2OLD  15023  isstruct2  15179  srngbase  15302  srngplusg  15303  srngmulr  15304  lmodbase  15311  lmodplusg  15312  lmodsca  15313  ipsbase  15318  ipsaddg  15319  ipsmulr  15320  phlbase  15328  phlplusg  15329  phlsca  15330  odrngbas  15354  odrngplusg  15355  odrngmulr  15356  prdssca  15403  prdsbas  15404  prdsplusg  15405  prdsmulr  15406  prdsvsca  15407  prdsip  15408  prdsle  15409  prdsds  15411  prdstset  15413  imasbas  15462  imasplusg  15467  imasmulr  15468  imassca  15469  imasvsca  15470  imasip  15471  imasbasOLD  15474  mreexexlem2d  15600  drsdirfi  16232  ipobas  16450  ipotset  16452  acsfiindd  16472  psdmrn  16502  dirdm  16529  gsumzsplit  17609  gsumsplit2  17611  gsumzunsnd  17637  gsum2dlem2  17652  dprdfadd  17702  dmdprdsplit2lem  17727  dmdprdsplit2  17728  dmdprdsplit  17729  dprdsplit  17730  ablfac1eulem  17754  lspun  18259  lspsolv  18415  lsppratlem3  18421  islbs3  18427  lbsextlem2  18431  lbsextlem4  18433  psrbagaddcl  18643  psrbas  18651  psrplusg  18654  psrmulr  18657  mplsubglem  18707  mplcoe1  18738  mplcoe5  18741  cnfldbas  19023  cnfldadd  19024  cnfldmul  19025  cnfldcj  19026  cnfldtset  19027  cnfldle  19028  cnfldds  19029  mdetunilem9  19694  basdif0  20017  ordtbas2  20256  ordtbas  20257  ordtopn1  20259  leordtval2  20277  iocpnfordt  20280  icomnfordt  20281  uncmp  20467  fiuncmp  20468  bwth  20474  locfincmp  20590  comppfsc  20596  1stckgenlem  20617  1stckgen  20618  ptbasin  20641  ptbasfi  20645  dfac14lem  20681  dfac14  20682  ptuncnv  20871  ptunhmeo  20872  ptcmpfi  20877  fbun  20904  trfil2  20951  ufprim  20973  ufileu  20983  filufint  20984  ufildr  20995  fmfnfm  21022  hausflim  21045  fclsfnflim  21091  alexsubALTlem4  21114  tmdgsum  21159  tsmsgsum  21202  tsmsres  21207  tsmssplit  21215  tsmsxplem1  21216  ustssco  21278  ustuqtop1  21305  prdsxmetlem  21432  prdsbl  21555  icccmplem2  21890  fsumcn  21951  cnmpt2pc  22005  rrxmetlem  22410  rrxmet  22411  rrxdstprj1  22412  ovolctb2  22494  ovolunnul  22502  ovolfiniun  22503  nulmbl2  22539  finiunmbl  22546  volfiniun  22549  icombl  22566  ioombl  22567  uniiccdif  22584  mbfres2  22650  itg2splitlem  22755  itg2split  22756  itgfsum  22833  itgsplit  22842  itgsplitioo  22844  dvreslem  22913  dvaddbr  22941  dvmulbr  22942  dvmptfsum  22976  lhop  23017  dvcnvrelem2  23019  mdegcl  23067  elplyr  23204  plyrem  23307  xrlimcnp  23943  fsumharmonic  23986  chtdif  24134  lgsdir2lem3  24302  lgsquadlem2  24332  dchrisum0lem1b  24402  pntrlog2bndlem6  24470  pntlemf  24492  ex-ss  25926  shsleji  27072  shsval2i  27089  ssjo  27149  sshhococi  27248  padct  28356  gsumle  28591  gsumvsca1  28594  gsumvsca2  28595  esumsplit  28923  esumpad2  28926  aean  29116  sxbrsigalem2  29157  bnj931  29631  subfacp1lem2b  29953  subfacp1lem3  29954  subfacp1lem5  29956  kur14lem7  29984  kur14lem9  29986  cvmliftlem10  30066  dftrpred3g  30523  nofulllem4  30643  refssfne  31063  filnetlem3  31085  bj-unrab  31574  bj-snglsstag  31620  bj-2upln0  31662  bj-ccssccbar  31704  finixpnum  31975  mbfresfi  32032  prdsbnd  32170  heibor1lem  32186  rrnequiv  32212  paddunssN  33418  sspadd1  33425  sspadd2  33426  pclfinN  33510  dochdmj1  35003  dvhdimlem  35057  elrfi  35581  mzpcompact2lem  35638  eldioph2  35649  eldioph4b  35699  ttac  35936  pwssplit4  35992  pwslnmlem2  35996  isnumbasgrplem2  36008  algbase  36089  algaddg  36090  algmulr  36091  fiuneneq  36116  idomsubgmo  36117  rclexi  36267  rtrclex  36269  trclubgNEW  36270  trclexi  36272  rtrclexi  36273  cnvrcl0  36277  cnvtrcl0  36278  dfrtrcl5  36281  trrelsuperrel2dg  36308  dfrcl2  36311  relexp0a  36353  relexpaddss  36355  trclimalb2  36363  frege83d  36385  frege131d  36401  compne  36837  mccllem  37715  cncfiooicclem1  37809  dvmptfprod  37858  dvnprodlem1  37859  iblsplit  37881  fourierdlem54  38062  fourierdlem102  38110  fourierdlem103  38111  fourierdlem104  38112  fourierdlem114  38122  sge0resplit  38286  sge0split  38289  sge0splitmpt  38291  sge0xaddlem1  38313  isomenndlem  38389  hoiprodp1  38448  hoidmvlelem1  38455  hoidmvlelem2  38456  hoidmvlelem3  38457  hoidmvlelem4  38458  nn0ssxnn0  39119  gsumsplit2f  40419
  Copyright terms: Public domain W3C validator