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

Theorem ssun2 3479
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 3478 . 2  |-  A  C_  ( A  u.  B
)
2 uncom 3459 . 2  |-  ( A  u.  B )  =  ( B  u.  A
)
31, 2sseqtri 3348 1  |-  A  C_  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    u. cun 3286    C_ wss 3288
This theorem is referenced by:  ssun4  3481  elun2  3483  nsspssun  3542  unv  3623  un00  3631  snsspr2  3916  snsstp3  3919  unexb  4676  difex2  4681  rnexg  5098  fvrn0  5720  fnsuppres  5919  brtpos0  6453  riotassuni  6555  oaabs2  6855  domunsncan  7175  mapunen  7243  ac6sfi  7318  unfir  7342  domunfican  7346  iunfi  7361  elfiun  7401  dffi3  7402  hartogslem1  7475  unwdomg  7516  unxpwdom2  7520  unxpwdom  7521  trcl  7628  unwf  7700  rankunb  7740  r0weon  7858  infxpenlem  7859  alephfplem4  7952  cda1dif  8020  cdainflem  8035  infcda  8052  cfsuc  8101  fin1a2lem10  8253  axdc3lem4  8297  ttukeylem7  8359  fpwwe2lem13  8481  canthp1lem2  8492  gchac  8512  wunrn  8568  wunex2  8577  inar1  8614  ltrelxr  9103  un0mulcl  10218  pnfxr  10677  hashbclem  11664  hashf1lem1  11667  ccatfn  11704  fsumsplit  12496  o1fsum  12555  incexclem  12579  vdwlem5  13316  vdwlem8  13319  ramcl2  13347  srnginvl  13551  lmodvsca  13560  algsca  13565  algvsca  13566  phlvsca  13575  phlip  13576  odrngtset  13601  odrngle  13602  odrngds  13603  prdssca  13642  prdsvsca  13646  prdsle  13647  prdsds  13649  prdstset  13651  prdshom  13652  prdsco  13653  imasds  13702  imassca  13708  imasvsca  13709  imastset  13710  imasle  13711  mreexexlemd  13832  mreexexlem2d  13833  mreexexlem3d  13834  drsdirfi  14358  ipolerval  14545  psdmrn  14602  dirge  14645  gsumzaddlem  15489  gsumzsplit  15492  gsumsplit2  15494  gsum2d  15509  dprdfadd  15541  dmdprdsplit2lem  15566  dmdprdsplit2  15567  dmdprdsplit  15568  dprdsplit  15569  ablfac1eulem  15593  pgpfaclem1  15602  lspun  16026  lbsextlem2  16194  lbsextlem3  16195  lbsextlem4  16196  psrbagaddcl  16398  psrsca  16416  psrvscafval  16417  mplsubglem  16461  mplcoe2  16493  opsrtoslem2  16508  cnfldcj  16673  cnfldtset  16674  cnfldle  16675  cnfldds  16676  cnfldunif  16677  ordtbas2  17217  ordtbas  17218  ordtopn1  17220  ordtopn2  17221  leordtval2  17238  icomnfordt  17242  iooordt  17243  perfcls  17391  uncmp  17428  fiuncmp  17429  2ndcdisj2  17481  1stckgenlem  17546  1stckgen  17547  ptbasin  17570  ptbasfi  17574  dfac14lem  17610  dfac14  17611  ptuncnv  17800  ptunhmeo  17801  ptcmpfi  17806  fbun  17833  filcon  17876  isufil2  17901  ufprim  17902  fin1aufil  17925  flimclslem  17977  flimfnfcls  18021  tmdgsum  18086  tsmsgsum  18129  tsmssplit  18142  tsmsxplem1  18143  trust  18220  prdsdsf  18358  prdsmet  18361  prdsbl  18482  cnmpt2pc  18914  ovolctb2  19349  ovolfiniun  19358  finiunmbl  19399  volfiniun  19402  uniioombllem3  19438  uniioombllem4  19439  mbfres2  19498  itg2splitlem  19601  itg2split  19602  itgsplit  19688  limcvallem  19719  ellimc2  19725  limccnp  19739  limccnp2  19740  limcco  19741  dvmptfsum  19820  lhop2  19860  lhop  19861  mdegcl  19953  elply2  20076  elplyd  20082  ply1term  20084  ply0  20088  plyaddlem1  20093  plymullem1  20094  plymullem  20096  mtest  20281  xrlimcnp  20768  jensen  20788  fsumharmonic  20811  chtdif  20902  lgsdir2lem3  21070  lgsquadlem2  21100  dchrisumlem2  21145  dchrisum0lem1b  21170  dchrisum0lem1  21171  pntrlog2bndlem6  21238  pntlemf  21260  eupap1  21659  shsleji  22833  shsval2i  22850  ssjo  22910  sshhococi  23009  esumsplit  24408  measun  24526  aean  24556  sxbrsigalem2  24597  subfacp1lem2a  24827  subfacp1lem3  24829  subfacp1lem5  24831  erdszelem8  24845  kur14lem7  24859  cvmliftlem10  24942  fprodsplit  25250  wfrlem14  25491  wfrlem16  25493  nofulllem4  25581  mblfinlem3  26153  refssfne  26272  comppfsc  26285  topjoin  26292  tailf  26302  prdsbnd  26400  heibor1lem  26416  mzpcompact2lem  26706  eldioph2  26718  eldioph4b  26770  ttac  27005  pwssplit4  27067  isnumbasgrplem2  27145  isnumbasabl  27147  dfacbasgrp  27149  fiuneneq  27389  bnj970  29036  bnj1137  29082  sspadd2  30310  pclfinN  30394  dochdmj1  31885
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2393
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2399  df-cleq 2405  df-clel 2408  df-nfc 2537  df-v 2926  df-un 3293  df-in 3295  df-ss 3302
  Copyright terms: Public domain W3C validator