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

Theorem ssun1 3572
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 386 . . 3  |-  ( x  e.  A  ->  (
x  e.  A  \/  x  e.  B )
)
2 elun 3549 . . 3  |-  ( x  e.  ( A  u.  B )  <->  ( x  e.  A  \/  x  e.  B ) )
31, 2sylibr 215 . 2  |-  ( x  e.  A  ->  x  e.  ( A  u.  B
) )
43ssriv 3411 1  |-  A  C_  ( A  u.  B
)
Colors of variables: wff setvar class
Syntax hints:    \/ wo 369    e. wcel 1872    u. cun 3377    C_ wss 3379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2063  ax-ext 2408
This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2558  df-v 3024  df-un 3384  df-in 3386  df-ss 3393
This theorem is referenced by:  ssun2  3573  ssun3  3574  elun1  3576  inabs  3647  reuun1  3698  un00  3773  snsspr1  4092  snsstp1  4094  snsstp2  4095  uniintsn  4236  sofld  5246  sssucid  5462  fvrn0  5847  ovima0  6406  unexb  6549  dmexg  6682  suppun  6890  dftpos2  6945  tpostpos2  6949  wfrlem14  7004  wfrlem15  7005  tfrlem11  7061  oaabs2  7301  ralxpmap  7476  domss2  7684  mapunen  7694  ac6sfi  7768  frfi  7769  unfir  7792  domunfican  7797  iunfi  7815  elfiun  7897  dffi3  7898  unwdomg  8052  unxpwdom2  8056  unxpwdom  8057  cantnfp1lem1  8135  cantnfp1lem3  8137  tc2  8178  unwf  8233  rankunb  8273  r0weon  8395  infxpenlem  8396  dfac2  8512  cdadom3  8569  cdainflem  8572  infunabs  8588  infcda  8589  infdif  8590  ackbij1lem15  8615  cfsmolem  8651  isfin4-3  8696  fin23lem11  8698  fin1a2lem10  8790  fin1a2lem13  8793  axdc3lem4  8834  axcclem  8838  zornn0g  8886  ttukeylem1  8890  ttukeylem5  8894  ttukeylem7  8896  fingch  8999  fpwwe2lem13  9018  gchac  9057  wunfi  9097  wundm  9104  wunex2  9114  inar1  9151  ressxr  9635  nnssnn0  10823  un0addcl  10854  un0mulcl  10855  hashbclem  12563  hashf1lem1  12566  hashf1lem2  12567  ccatfnOLD  12666  ccatrn  12681  trclublem  13003  relexpdmg  13049  relexpaddg  13060  fsumsplit  13749  fsum2d  13775  fsumabs  13804  fsumrlim  13814  fsumo1  13815  incexclem  13837  fprodsplit  13963  fprod2d  13978  lcmfunsnlem1  14553  coprmprod  14621  vdwapid1  14868  vdwlem6  14879  ramcl2  14916  ramcl2OLD  14917  isstruct2  15073  srngbase  15196  srngplusg  15197  srngmulr  15198  lmodbase  15205  lmodplusg  15206  lmodsca  15207  ipsbase  15212  ipsaddg  15213  ipsmulr  15214  phlbase  15222  phlplusg  15223  phlsca  15224  odrngbas  15248  odrngplusg  15249  odrngmulr  15250  prdssca  15297  prdsbas  15298  prdsplusg  15299  prdsmulr  15300  prdsvsca  15301  prdsip  15302  prdsle  15303  prdsds  15305  prdstset  15307  imasbas  15356  imasplusg  15361  imasmulr  15362  imassca  15363  imasvsca  15364  imasip  15365  imasbasOLD  15368  mreexexlem2d  15494  drsdirfi  16126  ipobas  16344  ipotset  16346  acsfiindd  16366  psdmrn  16396  dirdm  16423  gsumzsplit  17503  gsumsplit2  17505  gsumzunsnd  17531  gsum2dlem2  17546  dprdfadd  17596  dmdprdsplit2lem  17621  dmdprdsplit2  17622  dmdprdsplit  17623  dprdsplit  17624  ablfac1eulem  17648  lspun  18153  lspsolv  18309  lsppratlem3  18315  islbs3  18321  lbsextlem2  18325  lbsextlem4  18327  psrbagaddcl  18537  psrbas  18545  psrplusg  18548  psrmulr  18551  mplsubglem  18601  mplcoe1  18632  mplcoe5  18635  cnfldbas  18917  cnfldadd  18918  cnfldmul  18919  cnfldcj  18920  cnfldtset  18921  cnfldle  18922  cnfldds  18923  mdetunilem9  19587  basdif0  19910  ordtbas2  20149  ordtbas  20150  ordtopn1  20152  leordtval2  20170  iocpnfordt  20173  icomnfordt  20174  uncmp  20360  fiuncmp  20361  bwth  20367  locfincmp  20483  comppfsc  20489  1stckgenlem  20510  1stckgen  20511  ptbasin  20534  ptbasfi  20538  dfac14lem  20574  dfac14  20575  ptuncnv  20764  ptunhmeo  20765  ptcmpfi  20770  fbun  20797  trfil2  20844  ufprim  20866  ufileu  20876  filufint  20877  ufildr  20888  fmfnfm  20915  hausflim  20938  fclsfnflim  20984  alexsubALTlem4  21007  tmdgsum  21052  tsmsgsum  21095  tsmsres  21100  tsmssplit  21108  tsmsxplem1  21109  ustssco  21171  ustuqtop1  21198  prdsxmetlem  21325  prdsbl  21448  icccmplem2  21783  fsumcn  21844  cnmpt2pc  21898  rrxmetlem  22303  rrxmet  22304  rrxdstprj1  22305  ovolctb2  22387  ovolunnul  22395  ovolfiniun  22396  nulmbl2  22432  finiunmbl  22439  volfiniun  22442  icombl  22459  ioombl  22460  uniiccdif  22477  mbfres2  22543  itg2splitlem  22648  itg2split  22649  itgfsum  22726  itgsplit  22735  itgsplitioo  22737  dvreslem  22806  dvaddbr  22834  dvmulbr  22835  dvmptfsum  22869  lhop  22910  dvcnvrelem2  22912  mdegcl  22960  elplyr  23097  plyrem  23200  xrlimcnp  23836  fsumharmonic  23879  chtdif  24027  lgsdir2lem3  24195  lgsquadlem2  24225  dchrisum0lem1b  24295  pntrlog2bndlem6  24363  pntlemf  24385  ex-ss  25819  shsleji  26965  shsval2i  26982  ssjo  27042  sshhococi  27141  padct  28257  gsumle  28493  gsumvsca1  28497  gsumvsca2  28498  esumsplit  28826  esumpad2  28829  aean  29019  sxbrsigalem2  29060  bnj931  29534  subfacp1lem2b  29856  subfacp1lem3  29857  subfacp1lem5  29859  kur14lem7  29887  kur14lem9  29889  cvmliftlem10  29969  dftrpred3g  30425  nofulllem4  30543  refssfne  30963  filnetlem3  30985  bj-unrab  31440  bj-snglsstag  31486  bj-2upln0  31528  bj-ccssccbar  31566  finixpnum  31837  mbfresfi  31894  prdsbnd  32032  heibor1lem  32048  rrnequiv  32074  paddunssN  33285  sspadd1  33292  sspadd2  33293  pclfinN  33377  dochdmj1  34870  dvhdimlem  34924  elrfi  35448  mzpcompact2lem  35505  eldioph2  35516  eldioph4b  35566  ttac  35804  pwssplit4  35860  pwslnmlem2  35864  isnumbasgrplem2  35876  algbase  35957  algaddg  35958  algmulr  35959  fiuneneq  35984  idomsubgmo  35985  rclexi  36135  rtrclex  36137  trclubgNEW  36138  trclexi  36140  rtrclexi  36141  cnvrcl0  36145  cnvtrcl0  36146  dfrtrcl5  36149  trrelsuperrel2dg  36176  dfrcl2  36179  relexp0a  36221  relexpaddss  36223  trclimalb2  36231  frege83d  36253  frege131d  36269  compne  36706  mccllem  37560  cncfiooicclem1  37654  dvmptfprod  37703  dvnprodlem1  37704  iblsplit  37726  fourierdlem54  37907  fourierdlem102  37955  fourierdlem103  37956  fourierdlem104  37957  fourierdlem114  37967  sge0resplit  38099  sge0split  38102  sge0splitmpt  38104  sge0xaddlem1  38126  isomenndlem  38202  hoiprodp1  38257  hoidmvlelem1  38264  hoidmvlelem2  38265  hoidmvlelem3  38266  hoidmvlelem4  38267  gsumsplit2f  39749
  Copyright terms: Public domain W3C validator