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

Theorem ssun1 3248
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
StepHypRef Expression
1 orc 376 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3226 . . 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 3105 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    e. wcel 1621    u. cun 3076    C_ wss 3078
This theorem is referenced by:  ssun2  3249  ssun3  3250  elun1  3252  inabs  3307  reuun1  3357  un00  3397  snsspr1  3664  snsstp1  3666  snsstp2  3667  uniintsn  3797  sssucid  4362  unexb  4411  dmexg  4846  sofld  5028  fvrn0  5403  dftpos2  6103  tpostpos2  6107  riotassuni  6229  tfrlem11  6290  oaabs2  6529  ersym  6558  domss2  6905  mapunen  6915  ac6sfi  6986  frfi  6987  unfir  7010  domunfican  7014  iunfi  7029  finsschain  7046  elfiun  7067  dffi3  7068  unwdomg  7182  unxpwdom2  7186  unxpwdom  7187  cantnfp1lem1  7264  cantnfp1lem3  7266  tc2  7311  unwf  7366  rankunb  7406  r0weon  7524  infxpenlem  7525  dfac2  7641  cdadom3  7698  cdainflem  7701  infunabs  7717  infcda  7718  infdif  7719  ackbij1lem15  7744  ackbij1lem16  7745  cfsmolem  7780  isfin4-3  7825  fin23lem11  7827  fin1a2lem10  7919  fin1a2lem13  7922  axdc3lem4  7963  axcclem  7967  zornn0g  8016  ttukeylem1  8020  ttukeylem5  8024  ttukeylem7  8026  fingch  8125  fpwwe2lem13  8144  gchac  8175  wunfi  8223  wundm  8230  wunex2  8240  inar1  8277  ressxr  8756  nnssnn0  9847  un0addcl  9876  un0mulcl  9877  hashbclem  11267  hashf1lem1  11270  hashf1lem2  11271  ccatfn  11304  fsumsplit  12089  sumsplit  12108  fsum2d  12111  fsumabs  12136  fsumrlim  12146  fsumo1  12147  fsumiun  12156  vdwapid1  12896  vdwlem6  12907  ramcl2  12937  isstruct2  13031  srngbase  13138  srngplusg  13139  srngmulr  13140  lmodbase  13147  lmodplusg  13148  lmodsca  13149  algbase  13152  algaddg  13153  algmulr  13154  phlbase  13162  phlplusg  13163  phlsca  13164  odrngbas  13186  odrngplusg  13187  odrngmulr  13188  prdssca  13230  prdsbas  13231  prdsplusg  13232  prdsmulr  13233  prdsvsca  13234  prdsle  13235  prdsds  13237  prdstset  13239  imasbas  13289  imasplusg  13294  imasmulr  13295  imassca  13296  imasvsca  13297  yonedalem1  13890  yonedalem21  13891  yonedalem22  13896  yonffthlem  13900  drsdirfi  13916  ipobas  14102  ipotset  14104  psdmrn  14151  dirdm  14191  gsumzaddlem  15038  gsumzsplit  15041  gsumsplit2  15043  gsum2d  15058  dprdfadd  15090  dmdprdsplit2lem  15115  dmdprdsplit2  15116  dmdprdsplit  15117  dprdsplit  15118  ablfac1eulem  15142  lspun  15579  lsmsp  15674  lspsolv  15731  lsppratlem3  15736  islbs3  15742  lbsextlem2  15744  lbsextlem4  15746  psrbagaddcl  15948  psrbas  15956  psrplusg  15958  psrmulr  15961  mplsubglem  16011  mplcoe1  16041  mplcoe2  16043  cnfldbas  16215  cnfldadd  16216  cnfldmul  16217  cnfldcj  16218  basdif0  16523  tgdif0  16562  ordtbas2  16753  ordtbas  16754  ordtopn1  16756  leordtval2  16774  iocpnfordt  16777  icomnfordt  16778  uncmp  16962  fiuncmp  16963  1stckgenlem  17080  1stckgen  17081  ptbasin  17104  ptbasfi  17108  dfac14lem  17143  dfac14  17144  ptuncnv  17330  ptunhmeo  17331  ptcmpfi  17336  fbun  17367  trfil2  17414  isufil2  17435  ufprim  17436  ufileu  17446  filufint  17447  ufildr  17458  fmfnfm  17485  hausflim  17508  flimclslem  17511  fclsfnflim  17554  flimfnfcls  17555  alexsubALTlem4  17576  tmdgsum  17610  tsmsgsum  17653  tsmsres  17658  tsmssplit  17666  tsmsxplem1  17667  prdsxmetlem  17764  imasdsf1olem  17769  prdsbl  17869  icccmplem2  18160  fsumcn  18206  cnmpt2pc  18258  iccpnfcnv  18274  ovolctb2  18683  ovolunnul  18691  ovolfiniun  18692  nulmbl2  18726  finiunmbl  18733  volfiniun  18736  icombl  18753  ioombl  18754  uniiccdif  18765  mbfres2  18832  itg2splitlem  18935  itg2split  18936  itgfsum  19013  itgsplit  19022  itgsplitioo  19024  limcdif  19058  dvreslem  19091  dvaddbr  19119  dvmulbr  19120  dvmptfsum  19154  lhop  19195  dvcnvrelem2  19197  mdegcl  19287  elplyr  19415  plyrem  19517  xrlimcnp  20095  jensenlem1  20113  jensenlem2  20114  jensen  20115  fsumharmonic  20137  chtdif  20228  lgsdir2lem3  20396  lgsquadlem2  20426  dchrisum0lem1b  20496  pntrlog2bndlem6  20564  pntlemf  20586  ex-ss  20627  shsleji  21779  shsval2i  21796  ssjo  21856  sshhococi  21955  subfacp1lem2b  22883  subfacp1lem3  22884  subfacp1lem5  22886  kur14lem7  22914  kur14lem9  22916  cvmliftlem10  22996  dftrpred3g  23404  wfrlem14  23437  wfrlem15  23438  axfelem13  23526  domfldrefc  24222  prl  24333  basexre  24688  islimrs4  24748  segray  25321  refssfne  25460  locfincmp  25470  comppfsc  25473  filnetlem3  25495  prdsbnd  25683  heibor1lem  25699  rrnequiv  25725  ralxpmap  25927  elrfi  25935  mzpcompact2lem  25995  eldioph2  26007  eldioph4b  26060  ttac  26295  pwssplit4  26357  pwslnmlem2  26361  isnumbasgrplem2  26435  rngunsnply  26544  fiuneneq  26679  idomsubgmo  26680  compne  26809  bnj931  27588  paddunssN  28901  sspadd1  28908  sspadd2  28909  pclfinN  28993  dochdmj1  30484  dvhdimlem  30538
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-un 3083  df-in 3085  df-ss 3089
  Copyright terms: Public domain W3C validator