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

Theorem ssun1 3510
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 375 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3488 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 204 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3352 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 358    e. wcel 1725    u. cun 3318    C_ wss 3320
This theorem is referenced by:  ssun2  3511  ssun3  3512  elun1  3514  inabs  3572  reuun1  3623  un00  3663  snsspr1  3947  snsstp1  3949  snsstp2  3950  uniintsn  4087  sssucid  4658  unexb  4709  dmexg  5130  sofld  5318  fvrn0  5753  dftpos2  6496  tpostpos2  6500  riotassuni  6588  tfrlem11  6649  oaabs2  6888  domss2  7266  mapunen  7276  ac6sfi  7351  frfi  7352  unfir  7375  domunfican  7379  iunfi  7394  elfiun  7435  dffi3  7436  unwdomg  7552  unxpwdom2  7556  unxpwdom  7557  cantnfp1lem1  7634  cantnfp1lem3  7636  tc2  7681  unwf  7736  rankunb  7776  r0weon  7894  infxpenlem  7895  dfac2  8011  cdadom3  8068  cdainflem  8071  infunabs  8087  infcda  8088  infdif  8089  ackbij1lem15  8114  cfsmolem  8150  isfin4-3  8195  fin23lem11  8197  fin1a2lem10  8289  fin1a2lem13  8292  axdc3lem4  8333  axcclem  8337  zornn0g  8385  ttukeylem1  8389  ttukeylem5  8393  ttukeylem7  8395  fingch  8498  fpwwe2lem13  8517  gchac  8548  wunfi  8596  wundm  8603  wunex2  8613  inar1  8650  ressxr  9129  nnssnn0  10224  un0addcl  10253  un0mulcl  10254  hashbclem  11701  hashf1lem1  11704  hashf1lem2  11705  ccatfn  11741  fsumsplit  12533  fsum2d  12555  fsumabs  12580  fsumrlim  12590  fsumo1  12591  incexclem  12616  vdwapid1  13343  vdwlem6  13354  ramcl2  13384  isstruct2  13478  srngbase  13585  srngplusg  13586  srngmulr  13587  lmodbase  13594  lmodplusg  13595  lmodsca  13596  algbase  13599  algaddg  13600  algmulr  13601  phlbase  13609  phlplusg  13610  phlsca  13611  odrngbas  13635  odrngplusg  13636  odrngmulr  13637  prdssca  13679  prdsbas  13680  prdsplusg  13681  prdsmulr  13682  prdsvsca  13683  prdsle  13684  prdsds  13686  prdstset  13688  imasbas  13738  imasplusg  13743  imasmulr  13744  imassca  13745  imasvsca  13746  mreexexlem2d  13870  drsdirfi  14395  ipobas  14581  ipotset  14583  acsfiindd  14603  psdmrn  14639  dirdm  14679  gsumzaddlem  15526  gsumzsplit  15529  gsumsplit2  15531  gsum2d  15546  dprdfadd  15578  dmdprdsplit2lem  15603  dmdprdsplit2  15604  dmdprdsplit  15605  dprdsplit  15606  ablfac1eulem  15630  lspun  16063  lspsolv  16215  lsppratlem3  16221  islbs3  16227  lbsextlem2  16231  lbsextlem4  16233  psrbagaddcl  16435  psrbas  16443  psrplusg  16445  psrmulr  16448  mplsubglem  16498  mplcoe1  16528  mplcoe2  16530  cnfldbas  16707  cnfldadd  16708  cnfldmul  16709  cnfldcj  16710  cnfldtset  16711  cnfldle  16712  cnfldds  16713  basdif0  17018  tgdif0  17057  ordtbas2  17255  ordtbas  17256  ordtopn1  17258  leordtval2  17276  iocpnfordt  17279  icomnfordt  17280  uncmp  17466  fiuncmp  17467  1stckgenlem  17585  1stckgen  17586  ptbasin  17609  ptbasfi  17613  dfac14lem  17649  dfac14  17650  ptuncnv  17839  ptunhmeo  17840  ptcmpfi  17845  fbun  17872  trfil2  17919  ufprim  17941  ufileu  17951  filufint  17952  ufildr  17963  fmfnfm  17990  hausflim  18013  fclsfnflim  18059  alexsubALTlem4  18081  tmdgsum  18125  tsmsgsum  18168  tsmsres  18173  tsmssplit  18181  tsmsxplem1  18182  ustssco  18244  ustuqtop1  18271  prdsxmetlem  18398  prdsbl  18521  icccmplem2  18854  fsumcn  18900  cnmpt2pc  18953  iccpnfcnv  18969  ovolctb2  19388  ovolunnul  19396  ovolfiniun  19397  nulmbl2  19431  finiunmbl  19438  volfiniun  19441  icombl  19458  ioombl  19459  uniiccdif  19470  mbfres2  19537  itg2splitlem  19640  itg2split  19641  itgfsum  19718  itgsplit  19727  itgsplitioo  19729  dvreslem  19796  dvaddbr  19824  dvmulbr  19825  dvmptfsum  19859  lhop  19900  dvcnvrelem2  19902  mdegcl  19992  elplyr  20120  plyrem  20222  xrlimcnp  20807  fsumharmonic  20850  chtdif  20941  lgsdir2lem3  21109  lgsquadlem2  21139  dchrisum0lem1b  21209  pntrlog2bndlem6  21277  pntlemf  21299  ex-ss  21735  shsleji  22872  shsval2i  22889  ssjo  22949  sshhococi  23048  esumsplit  24447  aean  24595  sxbrsigalem2  24636  subfacp1lem2b  24867  subfacp1lem3  24868  subfacp1lem5  24870  kur14lem7  24898  kur14lem9  24900  cvmliftlem10  24981  fprodsplit  25289  fprod2d  25305  dftrpred3g  25511  wfrlem14  25551  wfrlem15  25552  nofulllem4  25660  mbfresfi  26253  refssfne  26374  locfincmp  26384  comppfsc  26387  filnetlem3  26409  prdsbnd  26502  heibor1lem  26518  rrnequiv  26544  ralxpmap  26742  elrfi  26748  mzpcompact2lem  26808  eldioph2  26820  eldioph4b  26872  ttac  27107  pwssplit4  27168  pwslnmlem2  27172  isnumbasgrplem2  27246  fiuneneq  27490  idomsubgmo  27491  compne  27619  bnj931  29141  paddunssN  30605  sspadd1  30612  sspadd2  30613  pclfinN  30697  dochdmj1  32188  dvhdimlem  32242
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2417
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-un 3325  df-in 3327  df-ss 3334
  Copyright terms: Public domain W3C validator