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

Theorem ssun1 3507
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 385 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3485 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 212 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3348 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    e. wcel 1755    u. cun 3314    C_ wss 3316
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1594  ax-4 1605  ax-5 1669  ax-6 1707  ax-7 1727  ax-10 1774  ax-11 1779  ax-12 1791  ax-13 1942  ax-ext 2414
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1365  df-ex 1590  df-nf 1593  df-sb 1700  df-clab 2420  df-cleq 2426  df-clel 2429  df-nfc 2558  df-v 2964  df-un 3321  df-in 3323  df-ss 3330
This theorem is referenced by:  ssun2  3508  ssun3  3509  elun1  3511  inabs  3569  reuun1  3620  un00  3702  snsspr1  4010  snsstp1  4012  snsstp2  4013  uniintsn  4153  sssucid  4783  sofld  5274  fvrn0  5700  ovima0  6231  unexb  6369  dmexg  6498  suppun  6698  dftpos2  6751  tpostpos2  6755  tfrlem11  6833  oaabs2  7072  ralxpmap  7250  domss2  7458  mapunen  7468  ac6sfi  7544  frfi  7545  unfir  7568  domunfican  7572  iunfi  7587  elfiun  7668  dffi3  7669  unwdomg  7787  unxpwdom2  7791  unxpwdom  7792  cantnfp1lem1  7874  cantnfp1lem3  7876  cantnfp1lem1OLD  7900  cantnfp1lem3OLD  7902  tc2  7950  unwf  8005  rankunb  8045  r0weon  8167  infxpenlem  8168  dfac2  8288  cdadom3  8345  cdainflem  8348  infunabs  8364  infcda  8365  infdif  8366  ackbij1lem15  8391  cfsmolem  8427  isfin4-3  8472  fin23lem11  8474  fin1a2lem10  8566  fin1a2lem13  8569  axdc3lem4  8610  axcclem  8614  zornn0g  8662  ttukeylem1  8666  ttukeylem5  8670  ttukeylem7  8672  fingch  8777  fpwwe2lem13  8796  gchac  8835  wunfi  8875  wundm  8882  wunex2  8892  inar1  8929  ressxr  9414  nnssnn0  10569  un0addcl  10600  un0mulcl  10601  hashbclem  12188  hashf1lem1  12191  hashf1lem2  12192  ccatfn  12255  fsumsplit  13199  fsum2d  13221  fsumabs  13246  fsumrlim  13256  fsumo1  13257  incexclem  13281  vdwapid1  14018  vdwlem6  14029  ramcl2  14059  isstruct2  14165  srngbase  14276  srngplusg  14277  srngmulr  14278  lmodbase  14285  lmodplusg  14286  lmodsca  14287  ipsbase  14292  ipsaddg  14293  ipsmulr  14294  phlbase  14302  phlplusg  14303  phlsca  14304  odrngbas  14328  odrngplusg  14329  odrngmulr  14330  prdssca  14376  prdsbas  14377  prdsplusg  14378  prdsmulr  14379  prdsvsca  14380  prdsip  14381  prdsle  14382  prdsds  14384  prdstset  14386  imasbas  14432  imasplusg  14437  imasmulr  14438  imassca  14439  imasvsca  14440  imasip  14441  mreexexlem2d  14565  drsdirfi  15090  ipobas  15307  ipotset  15309  acsfiindd  15329  psdmrn  15359  dirdm  15386  gsumzaddlemOLD  16389  gsumzsplit  16397  gsumzsplitOLD  16398  gsumsplit2  16401  gsumsplit2OLD  16402  gsum2dlem2  16435  gsum2dOLD  16437  dprdfadd  16483  dprdfaddOLD  16490  dmdprdsplit2lem  16517  dmdprdsplit2  16518  dmdprdsplit  16519  dprdsplit  16520  ablfac1eulem  16546  lspun  16989  lspsolv  17145  lsppratlem3  17151  islbs3  17157  lbsextlem2  17161  lbsextlem4  17163  psrbagaddcl  17371  psrbagaddclOLD  17372  psrbas  17381  psrbasOLD  17382  psrplusg  17385  psrmulr  17388  mplsubglem  17443  mplsubglemOLD  17445  mplcoe1  17477  mplcoe2  17480  mplcoe2OLD  17481  cnfldbas  17665  cnfldadd  17666  cnfldmul  17667  cnfldcj  17668  cnfldtset  17669  cnfldle  17670  cnfldds  17671  mdetunilem9  18267  basdif0  18399  tgdif0  18438  ordtbas2  18636  ordtbas  18637  ordtopn1  18639  leordtval2  18657  iocpnfordt  18660  icomnfordt  18661  uncmp  18847  fiuncmp  18848  bwth  18854  1stckgenlem  18967  1stckgen  18968  ptbasin  18991  ptbasfi  18995  dfac14lem  19031  dfac14  19032  ptuncnv  19221  ptunhmeo  19222  ptcmpfi  19227  fbun  19254  trfil2  19301  ufprim  19323  ufileu  19333  filufint  19334  ufildr  19345  fmfnfm  19372  hausflim  19395  fclsfnflim  19441  alexsubALTlem4  19463  tmdgsum  19507  tsmsgsum  19550  tsmsgsumOLD  19553  tsmsresOLD  19558  tsmsres  19559  tsmssplit  19567  tsmsxplem1  19568  ustssco  19630  ustuqtop1  19657  prdsxmetlem  19784  prdsbl  19907  icccmplem2  20241  fsumcn  20287  cnmpt2pc  20341  iccpnfcnv  20357  rrxmetlem  20747  rrxmet  20748  rrxdstprj1  20749  ovolctb2  20816  ovolunnul  20824  ovolfiniun  20825  nulmbl2  20859  finiunmbl  20866  volfiniun  20869  icombl  20886  ioombl  20887  uniiccdif  20899  mbfres2  20964  itg2splitlem  21067  itg2split  21068  itgfsum  21145  itgsplit  21154  itgsplitioo  21156  dvreslem  21225  dvaddbr  21253  dvmulbr  21254  dvmptfsum  21288  lhop  21329  dvcnvrelem2  21331  mdegcl  21424  elplyr  21553  plyrem  21655  xrlimcnp  22246  fsumharmonic  22289  chtdif  22380  lgsdir2lem3  22548  lgsquadlem2  22578  dchrisum0lem1b  22648  pntrlog2bndlem6  22716  pntlemf  22738  ex-ss  23456  shsleji  24595  shsval2i  24612  ssjo  24672  sshhococi  24771  gsumle  26097  gsummptun  26099  gsumvsca1  26103  gsumvsca2  26104  esumsplit  26359  aean  26513  sxbrsigalem2  26554  subfacp1lem2b  26916  subfacp1lem3  26917  subfacp1lem5  26919  kur14lem7  26947  kur14lem9  26949  cvmliftlem10  27030  fprodsplit  27322  fprod2d  27338  dftrpred3g  27543  wfrlem14  27583  wfrlem15  27584  nofulllem4  27692  finixpnum  28255  mbfresfi  28279  refssfne  28407  locfincmp  28417  comppfsc  28420  filnetlem3  28442  prdsbnd  28533  heibor1lem  28549  rrnequiv  28575  elrfi  28872  mzpcompact2lem  28930  eldioph2  28942  eldioph4b  28992  ttac  29227  pwssplit4  29284  pwslnmlem2  29288  isnumbasgrplem2  29302  algbase  29377  algaddg  29378  algmulr  29379  fiuneneq  29404  idomsubgmo  29405  compne  29538  bnj931  31463  bj-unrab  32012  bj-snglsstag  32054  bj-2upln0  32096  bj-ccssccbar  32117  paddunssN  33022  sspadd1  33029  sspadd2  33030  pclfinN  33114  dochdmj1  34605  dvhdimlem  34659
  Copyright terms: Public domain W3C validator