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

Theorem ssun2 3352
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 3351 . 2  |-  A  C_  ( A  u.  B
)
2 uncom 3332 . 2  |-  ( A  u.  B )  =  ( B  u.  A
)
31, 2sseqtri 3223 1  |-  A  C_  ( B  u.  A
)
Colors of variables: wff set class
Syntax hints:    u. cun 3163    C_ wss 3165
This theorem is referenced by:  ssun4  3354  elun2  3356  nsspssun  3415  unv  3495  un00  3503  snsspr2  3781  snsstp3  3784  unexb  4536  difex2  4541  rnexg  4956  fvrn0  5566  fnsuppres  5748  brtpos0  6257  riotassuni  6359  oaabs2  6659  ertr  6691  domunsncan  6978  mapunen  7046  ac6sfi  7117  unfir  7141  domunfican  7145  iunfi  7160  finsschain  7178  elfiun  7199  dffi3  7200  hartogslem1  7273  unwdomg  7314  unxpwdom2  7318  unxpwdom  7319  trcl  7426  unwf  7498  rankunb  7538  r0weon  7656  infxpenlem  7657  alephfplem4  7750  cda1dif  7818  cdainflem  7833  infcda  7850  ackbij1lem16  7877  cfsuc  7899  fin1a2lem10  8051  axdc3lem4  8095  ttukeylem7  8158  fpwwe2lem13  8280  canthp1lem2  8291  gchac  8311  wunfi  8359  wunrn  8367  wunex2  8376  inar1  8413  ltrelxr  8902  un0mulcl  10014  pnfxr  10471  hashbclem  11406  hashf1lem1  11409  hashf1lem2  11410  ccatfn  11443  fsumsplit  12228  sumsplit  12247  fsum2dlem  12249  fsumabs  12275  fsumrlim  12285  fsumo1  12286  o1fsum  12287  fsumiun  12295  incexclem  12311  vdwlem5  13048  vdwlem8  13051  ramcl2  13079  srnginvl  13283  lmodvsca  13292  algsca  13297  algvsca  13298  phlvsca  13307  phlip  13308  odrngtset  13331  odrngle  13332  odrngds  13333  prdssca  13372  prdsvsca  13376  prdsle  13377  prdsds  13379  prdstset  13381  prdshom  13382  prdsco  13383  imasds  13432  imassca  13438  imasvsca  13439  imastset  13440  imasle  13441  mreexexlemd  13562  mreexexlem2d  13563  mreexexlem3d  13564  yonedalem1  14062  yonedalem21  14063  yonedalem3a  14064  yonedalem4c  14067  yonedalem22  14068  yonedalem3b  14069  yonedainv  14071  yonffthlem  14072  drsdirfi  14088  ipolerval  14275  psdmrn  14332  dirge  14375  gsumzaddlem  15219  gsumzsplit  15222  gsumsplit2  15224  gsum2d  15239  dprdfadd  15271  dmdprdsplit2lem  15296  dmdprdsplit2  15297  dmdprdsplit  15298  dprdsplit  15299  ablfac1eulem  15323  pgpfaclem1  15332  lspun  15760  lsmsp  15855  lsppratlem3  15918  lbsextlem2  15928  lbsextlem3  15929  lbsextlem4  15930  psrbagaddcl  16132  psrsca  16150  psrvscafval  16151  mplsubglem  16195  mplcoe1  16225  mplcoe2  16227  opsrtoslem2  16242  cnfldcj  16402  cnfldtset  16403  cnfldle  16404  cnfldds  16405  ordtbas2  16937  ordtbas  16938  ordtopn1  16940  ordtopn2  16941  leordtval2  16958  icomnfordt  16962  iooordt  16963  perfcls  17109  uncmp  17146  fiuncmp  17147  2ndcdisj2  17199  1stckgenlem  17264  1stckgen  17265  ptbasin  17288  ptbasfi  17292  dfac14lem  17327  dfac14  17328  ptuncnv  17514  ptunhmeo  17515  ptcmpfi  17520  fbun  17551  filcon  17594  isufil2  17619  ufprim  17620  filufint  17631  fin1aufil  17643  fmfnfmlem4  17668  hausflim  17692  flimclslem  17695  fclsfnflim  17738  flimfnfcls  17739  tmdgsum  17794  tsmsgsum  17837  tsmssplit  17850  tsmsxplem1  17851  prdsdsf  17947  prdsmet  17950  prdsbl  18053  fsumcn  18390  cnmpt2pc  18442  ovolctb2  18867  ovolfiniun  18876  finiunmbl  18917  volfiniun  18920  uniioombllem3  18956  uniioombllem4  18957  mbfres2  19016  itg2splitlem  19119  itg2split  19120  itgfsum  19197  itgsplit  19206  limcvallem  19237  ellimc2  19243  limccnp  19257  limccnp2  19258  limcco  19259  dvmptfsum  19338  lhop2  19378  lhop  19379  mdegcl  19471  elply2  19594  elplyd  19600  ply1term  19602  ply0  19606  plyaddlem1  19611  plymullem1  19612  plymullem  19614  mtest  19797  xrlimcnp  20279  jensenlem1  20297  jensenlem2  20298  jensen  20299  fsumharmonic  20321  chtdif  20412  lgsdir2lem3  20580  lgsquadlem2  20610  dchrisumlem2  20655  dchrisum0lem1b  20680  dchrisum0lem1  20681  pntrlog2bndlem6  20748  pntlemf  20770  shsleji  21965  shsval2i  21982  ssjo  22042  sshhococi  22141  xrge0iifcnv  23330  esumsplit  23446  measxun  23554  subfacp1lem2a  23726  subfacp1lem3  23728  subfacp1lem5  23730  erdszelem8  23744  kur14lem7  23758  cvmliftlem10  23840  eupap1  23915  wfrlem14  24340  wfrlem16  24342  nofulllem4  24430  ranfldrefc  25161  refssfne  26397  comppfsc  26410  topjoin  26417  tailf  26427  prdsbnd  26620  heibor1lem  26636  mzpcompact2lem  26932  eldioph2  26944  eldioph4b  26997  ttac  27232  pwssplit4  27294  isnumbasgrplem2  27372  isnumbasabl  27374  dfacbasgrp  27376  rngunsnply  27481  fiuneneq  27616  bnj970  29295  bnj1137  29341  sspadd2  30627  pclfinN  30711  dochdmj1  32202
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-un 3170  df-in 3172  df-ss 3179
  Copyright terms: Public domain W3C validator