Theorem ssun2 3532

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

Step	Hyp	Ref	Expression
1		ssun1 3531	. 2 |- A C_ ( A u. B )
2		uncom 3512	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3400	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3338   C_ wss 3340

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2423

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2430  df-cleq 2436  df-clel 2439  df-nfc 2577  df-v 2986  df-un 3345  df-in 3347  df-ss 3354

This theorem is referenced by:  ssun4  3534  elun2  3536  nsspssun  3595  unv  3677  un00  3726  snsspr2  4035  snsstp3  4038  fvrn0  5724  fnsuppresOLD  5950  riotassuniOLD  6101  ovima0  6254  unexb  6392  difex2  6395  rnexg  6522  fnsuppres  6728  brtpos0  6764  oaabs2  7096  domunsncan  7423  mapunen  7492  ac6sfi  7568  unfir  7592  domunfican  7596  iunfi  7611  elfiun  7692  dffi3  7693  hartogslem1  7768  unwdomg  7811  unxpwdom2  7815  unxpwdom  7816  trcl  7960  unwf  8029  rankunb  8069  r0weon  8191  infxpenlem  8192  alephfplem4  8289  cda1dif  8357  cdainflem  8372  infcda  8389  cfsuc  8438  fin1a2lem10  8590  axdc3lem4  8634  ttukeylem7  8696  fpwwe2lem13  8821  canthp1lem2  8832  gchac  8860  wunrn  8908  wunex2  8917  inar1  8954  ltrelxr  9450  un0mulcl  10626  pnfxr  11104  fzdifsuc  11528  hashbclem  12217  hashf1lem1  12220  ccatfn  12284  fsumsplit  13228  o1fsum  13288  incexclem  13311  vdwlem5  14058  vdwlem8  14061  ramcl2  14089  srnginvl  14309  lmodvsca  14318  ipssca  14325  ipsvsca  14326  ipsip  14327  phlvsca  14335  phlip  14336  odrngtset  14361  odrngle  14362  odrngds  14363  prdssca  14406  prdsvsca  14410  prdsip  14411  prdsle  14412  prdsds  14414  prdstset  14416  prdshom  14417  prdsco  14418  imasds  14463  imassca  14469  imasvsca  14470  imasip  14471  imastset  14472  imasle  14473  mreexexlemd  14594  mreexexlem2d  14595  mreexexlem3d  14596  drsdirfi  15120  ipolerval  15338  psdmrn  15389  dirge  15419  gsumzaddlemOLD  16422  gsumzsplit  16430  gsumzsplitOLD  16431  gsumsplit2  16434  gsumsplit2OLD  16435  gsumzunsnd  16463  gsum2dlem2  16474  gsum2dOLD  16476  dprdfadd  16522  dprdfaddOLD  16529  dmdprdsplit2lem  16556  dmdprdsplit2  16557  dmdprdsplit  16558  dprdsplit  16559  ablfac1eulem  16585  pgpfaclem1  16594  lspun  17080  lbsextlem2  17252  lbsextlem3  17253  lbsextlem4  17254  psrbagaddcl  17450  psrbagaddclOLD  17451  psrsca  17472  psrvscafval  17473  mplsubglem  17522  mplsubglemOLD  17524  mplcoe5  17560  mplcoe2OLD  17562  opsrtoslem2  17578  cnfldcj  17837  cnfldtset  17838  cnfldle  17839  cnfldds  17840  cnfldunif  17841  ordtbas2  18807  ordtbas  18808  ordtopn1  18810  ordtopn2  18811  leordtval2  18828  icomnfordt  18832  iooordt  18833  perfcls  18981  uncmp  19018  fiuncmp  19019  2ndcdisj2  19073  1stckgenlem  19138  1stckgen  19139  ptbasin  19162  ptbasfi  19166  dfac14lem  19202  dfac14  19203  ptuncnv  19392  ptunhmeo  19393  ptcmpfi  19398  fbun  19425  filcon  19468  isufil2  19493  ufprim  19494  fin1aufil  19517  flimclslem  19569  flimfnfcls  19613  tmdgsum  19678  tsmsgsum  19721  tsmsgsumOLD  19724  tsmssplit  19738  tsmsxplem1  19739  trust  19816  prdsdsf  19954  prdsmet  19957  prdsbl  20078  cnmpt2pc  20512  rrxmetlem  20918  rrxmet  20919  rrxdstprj1  20920  ovolctb2  20987  ovolfiniun  20996  finiunmbl  21037  volfiniun  21040  uniioombllem3  21077  uniioombllem4  21078  mbfres2  21135  itg2splitlem  21238  itg2split  21239  itgsplit  21325  limcvallem  21358  ellimc2  21364  limccnp  21378  limccnp2  21379  limcco  21380  dvmptfsum  21459  lhop2  21499  lhop  21500  mdegcl  21552  elply2  21676  elplyd  21682  ply1term  21684  ply0  21688  plyaddlem1  21693  plymullem1  21694  plymullem  21696  mtest  21881  xrlimcnp  22374  jensen  22394  fsumharmonic  22417  chtdif  22508  lgsdir2lem3  22676  lgsquadlem2  22706  dchrisumlem2  22751  dchrisum0lem1b  22776  dchrisum0lem1  22777  pntrlog2bndlem6  22844  pntlemf  22866  eupap1  23609  shsleji  24785  shsval2i  24802  ssjo  24862  sshhococi  24961  gsumle  26258  gsummptun  26260  gsumvsca1  26263  gsumvsca2  26264  esumsplit  26518  measun  26637  aean  26672  sxbrsigalem2  26713  subfacp1lem2a  27080  subfacp1lem3  27082  subfacp1lem5  27084  erdszelem8  27098  kur14lem7  27112  cvmliftlem10  27195  fprodsplit  27488  wfrlem16  27751  nofulllem4  27858  finixpnum  28426  mblfinlem4  28443  refssfne  28578  comppfsc  28591  topjoin  28598  tailf  28608  prdsbnd  28704  heibor1lem  28720  mzpcompact2lem  29100  eldioph2  29112  eldioph4b  29162  ttac  29397  pwssplit4  29454  isnumbasgrplem2  29472  isnumbasabl  29474  dfacbasgrp  29476  algsca  29550  algvsca  29551  fiuneneq  29574  gsumsplit2f  30776  bnj970  31952  bnj1137  31998  bj-unrab  32441  bj-2upln1upl  32529  bj-ccinftyssccbar  32553  sspadd2  33472  pclfinN  33556  dochdmj1  35047