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

Theorem ssun1 3652
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 3630 . . 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 3493 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    e. wcel 1804    u. cun 3459    C_ wss 3461
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-13 1985  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-sb 1727  df-clab 2429  df-cleq 2435  df-clel 2438  df-nfc 2593  df-v 3097  df-un 3466  df-in 3468  df-ss 3475
This theorem is referenced by:  ssun2  3653  ssun3  3654  elun1  3656  inabs  3714  reuun1  3765  un00  3848  snsspr1  4164  snsstp1  4166  snsstp2  4167  uniintsn  4309  sssucid  4945  sofld  5445  fvrn0  5878  ovima0  6439  unexb  6585  dmexg  6716  suppun  6922  dftpos2  6974  tpostpos2  6978  tfrlem11  7059  oaabs2  7296  ralxpmap  7470  domss2  7678  mapunen  7688  ac6sfi  7766  frfi  7767  unfir  7790  domunfican  7795  iunfi  7810  elfiun  7892  dffi3  7893  unwdomg  8013  unxpwdom2  8017  unxpwdom  8018  cantnfp1lem1  8100  cantnfp1lem3  8102  cantnfp1lem1OLD  8126  cantnfp1lem3OLD  8128  tc2  8176  unwf  8231  rankunb  8271  r0weon  8393  infxpenlem  8394  dfac2  8514  cdadom3  8571  cdainflem  8574  infunabs  8590  infcda  8591  infdif  8592  ackbij1lem15  8617  cfsmolem  8653  isfin4-3  8698  fin23lem11  8700  fin1a2lem10  8792  fin1a2lem13  8795  axdc3lem4  8836  axcclem  8840  zornn0g  8888  ttukeylem1  8892  ttukeylem5  8896  ttukeylem7  8898  fingch  9004  fpwwe2lem13  9023  gchac  9062  wunfi  9102  wundm  9109  wunex2  9119  inar1  9156  ressxr  9640  nnssnn0  10805  un0addcl  10836  un0mulcl  10837  hashbclem  12482  hashf1lem1  12485  hashf1lem2  12486  ccatfn  12572  ccatrn  12587  fsumsplit  13543  fsum2d  13567  fsumabs  13596  fsumrlim  13606  fsumo1  13607  incexclem  13629  fprodsplit  13751  fprod2d  13766  vdwapid1  14474  vdwlem6  14485  ramcl2  14515  isstruct2  14622  srngbase  14734  srngplusg  14735  srngmulr  14736  lmodbase  14743  lmodplusg  14744  lmodsca  14745  ipsbase  14750  ipsaddg  14751  ipsmulr  14752  phlbase  14760  phlplusg  14761  phlsca  14762  odrngbas  14786  odrngplusg  14787  odrngmulr  14788  prdssca  14834  prdsbas  14835  prdsplusg  14836  prdsmulr  14837  prdsvsca  14838  prdsip  14839  prdsle  14840  prdsds  14842  prdstset  14844  imasbas  14890  imasplusg  14895  imasmulr  14896  imassca  14897  imasvsca  14898  imasip  14899  mreexexlem2d  15023  drsdirfi  15545  ipobas  15763  ipotset  15765  acsfiindd  15785  psdmrn  15815  dirdm  15842  gsumzaddlemOLD  16914  gsumzsplit  16922  gsumzsplitOLD  16923  gsumsplit2  16926  gsumsplit2OLD  16927  gsumzunsnd  16960  gsum2dlem2  16976  gsum2dOLD  16978  dprdfadd  17038  dprdfaddOLD  17045  dmdprdsplit2lem  17072  dmdprdsplit2  17073  dmdprdsplit  17074  dprdsplit  17075  ablfac1eulem  17101  lspun  17611  lspsolv  17767  lsppratlem3  17773  islbs3  17779  lbsextlem2  17783  lbsextlem4  17785  psrbagaddcl  17998  psrbagaddclOLD  17999  psrbas  18008  psrbasOLD  18009  psrplusg  18012  psrmulr  18015  mplsubglem  18071  mplsubglemOLD  18073  mplcoe1  18105  mplcoe5  18109  mplcoe2OLD  18111  cnfldbas  18402  cnfldadd  18403  cnfldmul  18404  cnfldcj  18405  cnfldtset  18406  cnfldle  18407  cnfldds  18408  mdetunilem9  19099  basdif0  19431  ordtbas2  19669  ordtbas  19670  ordtopn1  19672  leordtval2  19690  iocpnfordt  19693  icomnfordt  19694  uncmp  19880  fiuncmp  19881  bwth  19887  locfincmp  20004  comppfsc  20010  1stckgenlem  20031  1stckgen  20032  ptbasin  20055  ptbasfi  20059  dfac14lem  20095  dfac14  20096  ptuncnv  20285  ptunhmeo  20286  ptcmpfi  20291  fbun  20318  trfil2  20365  ufprim  20387  ufileu  20397  filufint  20398  ufildr  20409  fmfnfm  20436  hausflim  20459  fclsfnflim  20505  alexsubALTlem4  20527  tmdgsum  20571  tsmsgsum  20614  tsmsgsumOLD  20617  tsmsresOLD  20622  tsmsres  20623  tsmssplit  20631  tsmsxplem1  20632  ustssco  20694  ustuqtop1  20721  prdsxmetlem  20848  prdsbl  20971  icccmplem2  21305  fsumcn  21351  cnmpt2pc  21405  rrxmetlem  21811  rrxmet  21812  rrxdstprj1  21813  ovolctb2  21880  ovolunnul  21888  ovolfiniun  21889  nulmbl2  21924  finiunmbl  21931  volfiniun  21934  icombl  21951  ioombl  21952  uniiccdif  21964  mbfres2  22029  itg2splitlem  22132  itg2split  22133  itgfsum  22210  itgsplit  22219  itgsplitioo  22221  dvreslem  22290  dvaddbr  22318  dvmulbr  22319  dvmptfsum  22353  lhop  22394  dvcnvrelem2  22396  mdegcl  22446  elplyr  22575  plyrem  22677  xrlimcnp  23274  fsumharmonic  23317  chtdif  23408  lgsdir2lem3  23576  lgsquadlem2  23606  dchrisum0lem1b  23676  pntrlog2bndlem6  23744  pntlemf  23766  ex-ss  25124  shsleji  26264  shsval2i  26281  ssjo  26341  sshhococi  26440  gsumle  27747  gsumvsca1  27750  gsumvsca2  27751  esumsplit  28040  aean  28193  sxbrsigalem2  28234  subfacp1lem2b  28602  subfacp1lem3  28603  subfacp1lem5  28605  kur14lem7  28633  kur14lem9  28635  cvmliftlem10  28716  dftrpred3g  29291  wfrlem14  29331  wfrlem15  29332  nofulllem4  29440  finixpnum  30013  mbfresfi  30036  refssfne  30151  filnetlem3  30173  prdsbnd  30264  heibor1lem  30280  rrnequiv  30306  elrfi  30601  mzpcompact2lem  30659  eldioph2  30670  eldioph4b  30720  ttac  30953  pwssplit4  31010  pwslnmlem2  31014  isnumbasgrplem2  31028  algbase  31103  algaddg  31104  algmulr  31105  fiuneneq  31130  idomsubgmo  31131  compne  31303  cncfiooicclem1  31603  iblsplit  31655  fourierdlem54  31832  fourierdlem102  31880  fourierdlem103  31881  fourierdlem104  31882  fourierdlem114  31892  gsumsplit2f  32687  bnj931  33562  bj-unrab  34242  bj-snglsstag  34287  bj-2upln0  34329  bj-ccssccbar  34360  paddunssN  35272  sspadd1  35279  sspadd2  35280  pclfinN  35364  dochdmj1  36857  dvhdimlem  36911  trclubg  37478
  Copyright terms: Public domain W3C validator