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

Theorem ssun1 3667
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 3645 . . 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 3508 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 368    e. wcel 1767    u. cun 3474    C_ wss 3476
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490
This theorem is referenced by:  ssun2  3668  ssun3  3669  elun1  3671  inabs  3729  reuun1  3780  un00  3862  snsspr1  4176  snsstp1  4178  snsstp2  4179  uniintsn  4319  sssucid  4955  sofld  5455  fvrn0  5888  ovima0  6438  unexb  6584  dmexg  6715  suppun  6920  dftpos2  6972  tpostpos2  6976  tfrlem11  7057  oaabs2  7294  ralxpmap  7468  domss2  7676  mapunen  7686  ac6sfi  7764  frfi  7765  unfir  7788  domunfican  7793  iunfi  7808  elfiun  7890  dffi3  7891  unwdomg  8010  unxpwdom2  8014  unxpwdom  8015  cantnfp1lem1  8097  cantnfp1lem3  8099  cantnfp1lem1OLD  8123  cantnfp1lem3OLD  8125  tc2  8173  unwf  8228  rankunb  8268  r0weon  8390  infxpenlem  8391  dfac2  8511  cdadom3  8568  cdainflem  8571  infunabs  8587  infcda  8588  infdif  8589  ackbij1lem15  8614  cfsmolem  8650  isfin4-3  8695  fin23lem11  8697  fin1a2lem10  8789  fin1a2lem13  8792  axdc3lem4  8833  axcclem  8837  zornn0g  8885  ttukeylem1  8889  ttukeylem5  8893  ttukeylem7  8895  fingch  9001  fpwwe2lem13  9020  gchac  9059  wunfi  9099  wundm  9106  wunex2  9116  inar1  9153  ressxr  9637  nnssnn0  10798  un0addcl  10829  un0mulcl  10830  hashbclem  12467  hashf1lem1  12470  hashf1lem2  12471  ccatfn  12556  fsumsplit  13525  fsum2d  13549  fsumabs  13578  fsumrlim  13588  fsumo1  13589  incexclem  13611  vdwapid1  14352  vdwlem6  14363  ramcl2  14393  isstruct2  14499  srngbase  14611  srngplusg  14612  srngmulr  14613  lmodbase  14620  lmodplusg  14621  lmodsca  14622  ipsbase  14627  ipsaddg  14628  ipsmulr  14629  phlbase  14637  phlplusg  14638  phlsca  14639  odrngbas  14663  odrngplusg  14664  odrngmulr  14665  prdssca  14711  prdsbas  14712  prdsplusg  14713  prdsmulr  14714  prdsvsca  14715  prdsip  14716  prdsle  14717  prdsds  14719  prdstset  14721  imasbas  14767  imasplusg  14772  imasmulr  14773  imassca  14774  imasvsca  14775  imasip  14776  mreexexlem2d  14900  drsdirfi  15425  ipobas  15642  ipotset  15644  acsfiindd  15664  psdmrn  15694  dirdm  15721  gsumzaddlemOLD  16739  gsumzsplit  16747  gsumzsplitOLD  16748  gsumsplit2  16751  gsumsplit2OLD  16752  gsumzunsnd  16785  gsum2dlem2  16801  gsum2dOLD  16803  dprdfadd  16862  dprdfaddOLD  16869  dmdprdsplit2lem  16896  dmdprdsplit2  16897  dmdprdsplit  16898  dprdsplit  16899  ablfac1eulem  16925  lspun  17433  lspsolv  17589  lsppratlem3  17595  islbs3  17601  lbsextlem2  17605  lbsextlem4  17607  psrbagaddcl  17819  psrbagaddclOLD  17820  psrbas  17829  psrbasOLD  17830  psrplusg  17833  psrmulr  17836  mplsubglem  17892  mplsubglemOLD  17894  mplcoe1  17926  mplcoe5  17930  mplcoe2OLD  17932  cnfldbas  18223  cnfldadd  18224  cnfldmul  18225  cnfldcj  18226  cnfldtset  18227  cnfldle  18228  cnfldds  18229  mdetunilem9  18917  basdif0  19249  tgdif0  19288  ordtbas2  19486  ordtbas  19487  ordtopn1  19489  leordtval2  19507  iocpnfordt  19510  icomnfordt  19511  uncmp  19697  fiuncmp  19698  bwth  19704  1stckgenlem  19817  1stckgen  19818  ptbasin  19841  ptbasfi  19845  dfac14lem  19881  dfac14  19882  ptuncnv  20071  ptunhmeo  20072  ptcmpfi  20077  fbun  20104  trfil2  20151  ufprim  20173  ufileu  20183  filufint  20184  ufildr  20195  fmfnfm  20222  hausflim  20245  fclsfnflim  20291  alexsubALTlem4  20313  tmdgsum  20357  tsmsgsum  20400  tsmsgsumOLD  20403  tsmsresOLD  20408  tsmsres  20409  tsmssplit  20417  tsmsxplem1  20418  ustssco  20480  ustuqtop1  20507  prdsxmetlem  20634  prdsbl  20757  icccmplem2  21091  fsumcn  21137  cnmpt2pc  21191  iccpnfcnv  21207  rrxmetlem  21597  rrxmet  21598  rrxdstprj1  21599  ovolctb2  21666  ovolunnul  21674  ovolfiniun  21675  nulmbl2  21710  finiunmbl  21717  volfiniun  21720  icombl  21737  ioombl  21738  uniiccdif  21750  mbfres2  21815  itg2splitlem  21918  itg2split  21919  itgfsum  21996  itgsplit  22005  itgsplitioo  22007  dvreslem  22076  dvaddbr  22104  dvmulbr  22105  dvmptfsum  22139  lhop  22180  dvcnvrelem2  22182  mdegcl  22232  elplyr  22361  plyrem  22463  xrlimcnp  23054  fsumharmonic  23097  chtdif  23188  lgsdir2lem3  23356  lgsquadlem2  23386  dchrisum0lem1b  23456  pntrlog2bndlem6  23524  pntlemf  23546  ex-ss  24853  shsleji  25992  shsval2i  26009  ssjo  26069  sshhococi  26168  gsumle  27461  gsumvsca1  27464  gsumvsca2  27465  esumsplit  27731  aean  27884  sxbrsigalem2  27925  subfacp1lem2b  28293  subfacp1lem3  28294  subfacp1lem5  28296  kur14lem7  28324  kur14lem9  28326  cvmliftlem10  28407  fprodsplit  28700  fprod2d  28716  dftrpred3g  28921  wfrlem14  28961  wfrlem15  28962  nofulllem4  29070  finixpnum  29643  mbfresfi  29666  refssfne  29794  locfincmp  29804  comppfsc  29807  filnetlem3  29829  prdsbnd  29920  heibor1lem  29936  rrnequiv  29962  elrfi  30258  mzpcompact2lem  30316  eldioph2  30327  eldioph4b  30377  ttac  30610  pwssplit4  30667  pwslnmlem2  30671  isnumbasgrplem2  30685  algbase  30760  algaddg  30761  algmulr  30762  fiuneneq  30787  idomsubgmo  30788  compne  30955  cncfiooicclem1  31260  iblsplit  31312  fourierdlem54  31489  fourierdlem102  31537  fourierdlem103  31538  fourierdlem104  31539  fourierdlem114  31549  gsumsplit2f  32051  bnj931  32926  bj-unrab  33593  bj-snglsstag  33638  bj-2upln0  33680  bj-ccssccbar  33710  paddunssN  34622  sspadd1  34629  sspadd2  34630  pclfinN  34714  dochdmj1  36205  dvhdimlem  36259  trclubg  36813
  Copyright terms: Public domain W3C validator