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

Theorem ssun1 3299
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 3277 . . 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 3145 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff set class
Syntax hints:    \/ wo 359    e. wcel 1621    u. cun 3111    C_ wss 3113
This theorem is referenced by:  ssun2  3300  ssun3  3301  elun1  3303  inabs  3361  reuun1  3411  un00  3451  snsspr1  3724  snsstp1  3726  snsstp2  3727  uniintsn  3859  sssucid  4427  unexb  4478  dmexg  4913  sofld  5095  fvrn0  5470  dftpos2  6171  tpostpos2  6175  riotassuni  6297  tfrlem11  6358  oaabs2  6597  ersym  6626  domss2  6974  mapunen  6984  ac6sfi  7055  frfi  7056  unfir  7079  domunfican  7083  iunfi  7098  finsschain  7116  elfiun  7137  dffi3  7138  unwdomg  7252  unxpwdom2  7256  unxpwdom  7257  cantnfp1lem1  7334  cantnfp1lem3  7336  tc2  7381  unwf  7436  rankunb  7476  r0weon  7594  infxpenlem  7595  dfac2  7711  cdadom3  7768  cdainflem  7771  infunabs  7787  infcda  7788  infdif  7789  ackbij1lem15  7814  ackbij1lem16  7815  cfsmolem  7850  isfin4-3  7895  fin23lem11  7897  fin1a2lem10  7989  fin1a2lem13  7992  axdc3lem4  8033  axcclem  8037  zornn0g  8086  ttukeylem1  8090  ttukeylem5  8094  ttukeylem7  8096  fingch  8199  fpwwe2lem13  8218  gchac  8249  wunfi  8297  wundm  8304  wunex2  8314  inar1  8351  ressxr  8830  nnssnn0  9921  un0addcl  9950  un0mulcl  9951  hashbclem  11341  hashf1lem1  11344  hashf1lem2  11345  ccatfn  11378  fsumsplit  12163  sumsplit  12182  fsum2d  12185  fsumabs  12210  fsumrlim  12220  fsumo1  12221  fsumiun  12230  vdwapid1  12970  vdwlem6  12981  ramcl2  13011  isstruct2  13105  srngbase  13212  srngplusg  13213  srngmulr  13214  lmodbase  13221  lmodplusg  13222  lmodsca  13223  algbase  13226  algaddg  13227  algmulr  13228  phlbase  13236  phlplusg  13237  phlsca  13238  odrngbas  13260  odrngplusg  13261  odrngmulr  13262  prdssca  13304  prdsbas  13305  prdsplusg  13306  prdsmulr  13307  prdsvsca  13308  prdsle  13309  prdsds  13311  prdstset  13313  imasbas  13363  imasplusg  13368  imasmulr  13369  imassca  13370  imasvsca  13371  mreexexlem2d  13495  yonedalem1  13994  yonedalem21  13995  yonedalem22  14000  yonffthlem  14004  drsdirfi  14020  ipobas  14206  ipotset  14208  acsfiindd  14228  psdmrn  14264  dirdm  14304  gsumzaddlem  15151  gsumzsplit  15154  gsumsplit2  15156  gsum2d  15171  dprdfadd  15203  dmdprdsplit2lem  15228  dmdprdsplit2  15229  dmdprdsplit  15230  dprdsplit  15231  ablfac1eulem  15255  lspun  15692  lsmsp  15787  lspsolv  15844  lsppratlem3  15850  islbs3  15856  lbsextlem2  15860  lbsextlem4  15862  psrbagaddcl  16064  psrbas  16072  psrplusg  16074  psrmulr  16077  mplsubglem  16127  mplcoe1  16157  mplcoe2  16159  cnfldbas  16331  cnfldadd  16332  cnfldmul  16333  cnfldcj  16334  basdif0  16639  tgdif0  16678  ordtbas2  16869  ordtbas  16870  ordtopn1  16872  leordtval2  16890  iocpnfordt  16893  icomnfordt  16894  uncmp  17078  fiuncmp  17079  1stckgenlem  17196  1stckgen  17197  ptbasin  17220  ptbasfi  17224  dfac14lem  17259  dfac14  17260  ptuncnv  17446  ptunhmeo  17447  ptcmpfi  17452  fbun  17483  trfil2  17530  isufil2  17551  ufprim  17552  ufileu  17562  filufint  17563  ufildr  17574  fmfnfm  17601  hausflim  17624  flimclslem  17627  fclsfnflim  17670  flimfnfcls  17671  alexsubALTlem4  17692  tmdgsum  17726  tsmsgsum  17769  tsmsres  17774  tsmssplit  17782  tsmsxplem1  17783  prdsxmetlem  17880  imasdsf1olem  17885  prdsbl  17985  icccmplem2  18276  fsumcn  18322  cnmpt2pc  18374  iccpnfcnv  18390  ovolctb2  18799  ovolunnul  18807  ovolfiniun  18808  nulmbl2  18842  finiunmbl  18849  volfiniun  18852  icombl  18869  ioombl  18870  uniiccdif  18881  mbfres2  18948  itg2splitlem  19051  itg2split  19052  itgfsum  19129  itgsplit  19138  itgsplitioo  19140  limcdif  19174  dvreslem  19207  dvaddbr  19235  dvmulbr  19236  dvmptfsum  19270  lhop  19311  dvcnvrelem2  19313  mdegcl  19403  elplyr  19531  plyrem  19633  xrlimcnp  20211  jensenlem1  20229  jensenlem2  20230  jensen  20231  fsumharmonic  20253  chtdif  20344  lgsdir2lem3  20512  lgsquadlem2  20542  dchrisum0lem1b  20612  pntrlog2bndlem6  20680  pntlemf  20702  ex-ss  20743  shsleji  21895  shsval2i  21912  ssjo  21972  sshhococi  22071  subfacp1lem2b  23070  subfacp1lem3  23071  subfacp1lem5  23073  kur14lem7  23101  kur14lem9  23103  cvmliftlem10  23183  dftrpred3g  23591  wfrlem14  23624  wfrlem15  23625  axfelem13  23713  domfldrefc  24409  prl  24520  basexre  24875  islimrs4  24935  segray  25508  refssfne  25647  locfincmp  25657  comppfsc  25660  filnetlem3  25682  prdsbnd  25870  heibor1lem  25886  rrnequiv  25912  ralxpmap  26114  elrfi  26122  mzpcompact2lem  26182  eldioph2  26194  eldioph4b  26247  ttac  26482  pwssplit4  26544  pwslnmlem2  26548  isnumbasgrplem2  26622  rngunsnply  26731  fiuneneq  26866  idomsubgmo  26867  compne  26996  bnj931  27835  paddunssN  29148  sspadd1  29155  sspadd2  29156  pclfinN  29240  dochdmj1  30731  dvhdimlem  30785
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 1927  ax-ext 2237
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 1884  df-clab 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2759  df-un 3118  df-in 3120  df-ss 3127
  Copyright terms: Public domain W3C validator