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

Theorem ssun2 3513
Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
ssun2  |-  A  C_  ( B  u.  A
)

Proof of Theorem ssun2
StepHypRef Expression
1 ssun1 3512 . 2  |-  A  C_  ( A  u.  B
)
2 uncom 3493 . 2  |-  ( A  u.  B )  =  ( B  u.  A
)
31, 2sseqtri 3382 1  |-  A  C_  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    u. cun 3320    C_ wss 3322
This theorem is referenced by:  ssun4  3515  elun2  3517  nsspssun  3576  unv  3657  un00  3665  snsspr2  3950  snsstp3  3953  unexb  4712  difex2  4717  rnexg  5134  fvrn0  5756  fnsuppres  5955  brtpos0  6489  riotassuni  6591  oaabs2  6891  domunsncan  7211  mapunen  7279  ac6sfi  7354  unfir  7378  domunfican  7382  iunfi  7397  elfiun  7438  dffi3  7439  hartogslem1  7514  unwdomg  7555  unxpwdom2  7559  unxpwdom  7560  trcl  7667  unwf  7739  rankunb  7779  r0weon  7899  infxpenlem  7900  alephfplem4  7993  cda1dif  8061  cdainflem  8076  infcda  8093  cfsuc  8142  fin1a2lem10  8294  axdc3lem4  8338  ttukeylem7  8400  fpwwe2lem13  8522  canthp1lem2  8533  gchac  8561  wunrn  8609  wunex2  8618  inar1  8655  ltrelxr  9144  un0mulcl  10259  pnfxr  10718  hashbclem  11706  hashf1lem1  11709  ccatfn  11746  fsumsplit  12538  o1fsum  12597  incexclem  12621  vdwlem5  13358  vdwlem8  13361  ramcl2  13389  srnginvl  13593  lmodvsca  13602  algsca  13607  algvsca  13608  phlvsca  13617  phlip  13618  odrngtset  13643  odrngle  13644  odrngds  13645  prdssca  13684  prdsvsca  13688  prdsle  13689  prdsds  13691  prdstset  13693  prdshom  13694  prdsco  13695  imasds  13744  imassca  13750  imasvsca  13751  imastset  13752  imasle  13753  mreexexlemd  13874  mreexexlem2d  13875  mreexexlem3d  13876  drsdirfi  14400  ipolerval  14587  psdmrn  14644  dirge  14687  gsumzaddlem  15531  gsumzsplit  15534  gsumsplit2  15536  gsum2d  15551  dprdfadd  15583  dmdprdsplit2lem  15608  dmdprdsplit2  15609  dmdprdsplit  15610  dprdsplit  15611  ablfac1eulem  15635  pgpfaclem1  15644  lspun  16068  lbsextlem2  16236  lbsextlem3  16237  lbsextlem4  16238  psrbagaddcl  16440  psrsca  16458  psrvscafval  16459  mplsubglem  16503  mplcoe2  16535  opsrtoslem2  16550  cnfldcj  16715  cnfldtset  16716  cnfldle  16717  cnfldds  16718  cnfldunif  16719  ordtbas2  17260  ordtbas  17261  ordtopn1  17263  ordtopn2  17264  leordtval2  17281  icomnfordt  17285  iooordt  17286  perfcls  17434  uncmp  17471  fiuncmp  17472  2ndcdisj2  17525  1stckgenlem  17590  1stckgen  17591  ptbasin  17614  ptbasfi  17618  dfac14lem  17654  dfac14  17655  ptuncnv  17844  ptunhmeo  17845  ptcmpfi  17850  fbun  17877  filcon  17920  isufil2  17945  ufprim  17946  fin1aufil  17969  flimclslem  18021  flimfnfcls  18065  tmdgsum  18130  tsmsgsum  18173  tsmssplit  18186  tsmsxplem1  18187  trust  18264  prdsdsf  18402  prdsmet  18405  prdsbl  18526  cnmpt2pc  18958  ovolctb2  19393  ovolfiniun  19402  finiunmbl  19443  volfiniun  19446  uniioombllem3  19482  uniioombllem4  19483  mbfres2  19540  itg2splitlem  19643  itg2split  19644  itgsplit  19730  limcvallem  19763  ellimc2  19769  limccnp  19783  limccnp2  19784  limcco  19785  dvmptfsum  19864  lhop2  19904  lhop  19905  mdegcl  19997  elply2  20120  elplyd  20126  ply1term  20128  ply0  20132  plyaddlem1  20137  plymullem1  20138  plymullem  20140  mtest  20325  xrlimcnp  20812  jensen  20832  fsumharmonic  20855  chtdif  20946  lgsdir2lem3  21114  lgsquadlem2  21144  dchrisumlem2  21189  dchrisum0lem1b  21214  dchrisum0lem1  21215  pntrlog2bndlem6  21282  pntlemf  21304  eupap1  21703  shsleji  22877  shsval2i  22894  ssjo  22954  sshhococi  23053  esumsplit  24452  measun  24570  aean  24600  sxbrsigalem2  24641  subfacp1lem2a  24871  subfacp1lem3  24873  subfacp1lem5  24875  erdszelem8  24889  kur14lem7  24903  cvmliftlem10  24986  fprodsplit  25294  wfrlem16  25558  nofulllem4  25665  mblfinlem4  26258  refssfne  26388  comppfsc  26401  topjoin  26408  tailf  26418  prdsbnd  26516  heibor1lem  26532  mzpcompact2lem  26822  eldioph2  26834  eldioph4b  26886  ttac  27121  pwssplit4  27182  isnumbasgrplem2  27260  isnumbasabl  27262  dfacbasgrp  27264  fiuneneq  27504  bnj970  29392  bnj1137  29438  sspadd2  30687  pclfinN  30771  dochdmj1  32262
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1556  ax-5 1567  ax-17 1627  ax-9 1667  ax-8 1688  ax-6 1745  ax-7 1750  ax-11 1762  ax-12 1951  ax-ext 2419
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1329  df-ex 1552  df-nf 1555  df-sb 1660  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2960  df-un 3327  df-in 3329  df-ss 3336
  Copyright terms: Public domain W3C validator