Theorem ssun2 3668

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 3667	. 2 |- A C_ ( A u. B )
2		uncom 3648	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3536	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3474   C_ wss 3476

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-un 3481  df-in 3483  df-ss 3490

This theorem is referenced by:  ssun4  3670  elun2  3672  nsspssun  3731  unv  3813  un00  3862  snsspr2  4177  snsstp3  4180  fvrn0  5887  fnsuppresOLD  6120  riotassuniOLD  6281  ovima0  6437  unexb  6583  difex2  6586  rnexg  6716  fnsuppres  6927  brtpos0  6962  oaabs2  7294  domunsncan  7617  mapunen  7686  ac6sfi  7763  unfir  7787  domunfican  7792  iunfi  7807  elfiun  7889  dffi3  7890  hartogslem1  7966  unwdomg  8009  unxpwdom2  8013  unxpwdom  8014  trcl  8158  unwf  8227  rankunb  8267  r0weon  8389  infxpenlem  8390  alephfplem4  8487  cda1dif  8555  cdainflem  8570  infcda  8587  cfsuc  8636  fin1a2lem10  8788  axdc3lem4  8832  ttukeylem7  8894  fpwwe2lem13  9019  canthp1lem2  9030  gchac  9058  wunrn  9106  wunex2  9115  inar1  9152  ltrelxr  9647  un0mulcl  10829  pnfxr  11320  fzdifsuc  11738  hashbclem  12466  hashf1lem1  12469  ccatfn  12555  fsumsplit  13524  o1fsum  13589  incexclem  13610  vdwlem5  14361  vdwlem8  14364  ramcl2  14392  srnginvl  14613  lmodvsca  14622  ipssca  14629  ipsvsca  14630  ipsip  14631  phlvsca  14639  phlip  14640  odrngtset  14665  odrngle  14666  odrngds  14667  prdssca  14710  prdsvsca  14714  prdsip  14715  prdsle  14716  prdsds  14718  prdstset  14720  prdshom  14721  prdsco  14722  imasds  14767  imassca  14773  imasvsca  14774  imasip  14775  imastset  14776  imasle  14777  mreexexlemd  14898  mreexexlem2d  14899  mreexexlem3d  14900  drsdirfi  15424  ipolerval  15642  psdmrn  15693  dirge  15723  gsumzaddlemOLD  16736  gsumzsplit  16744  gsumzsplitOLD  16745  gsumsplit2  16748  gsumsplit2OLD  16749  gsumzunsnd  16782  gsum2dlem2  16798  gsum2dOLD  16800  dprdfadd  16859  dprdfaddOLD  16866  dmdprdsplit2lem  16893  dmdprdsplit2  16894  dmdprdsplit  16895  dprdsplit  16896  ablfac1eulem  16922  pgpfaclem1  16931  lspun  17428  lbsextlem2  17600  lbsextlem3  17601  lbsextlem4  17602  psrbagaddcl  17807  psrbagaddclOLD  17808  psrsca  17829  psrvscafval  17830  mplsubglem  17880  mplsubglemOLD  17882  mplcoe5  17918  mplcoe2OLD  17920  opsrtoslem2  17936  cnfldcj  18214  cnfldtset  18215  cnfldle  18216  cnfldds  18217  cnfldunif  18218  ordtbas2  19474  ordtbas  19475  ordtopn1  19477  ordtopn2  19478  leordtval2  19495  icomnfordt  19499  iooordt  19500  perfcls  19648  uncmp  19685  fiuncmp  19686  2ndcdisj2  19740  1stckgenlem  19805  1stckgen  19806  ptbasin  19829  ptbasfi  19833  dfac14lem  19869  dfac14  19870  ptuncnv  20059  ptunhmeo  20060  ptcmpfi  20065  fbun  20092  filcon  20135  isufil2  20160  ufprim  20161  fin1aufil  20184  flimclslem  20236  flimfnfcls  20280  tmdgsum  20345  tsmsgsum  20388  tsmsgsumOLD  20391  tsmssplit  20405  tsmsxplem1  20406  trust  20483  prdsdsf  20621  prdsmet  20624  prdsbl  20745  cnmpt2pc  21179  rrxmetlem  21585  rrxmet  21586  rrxdstprj1  21587  ovolctb2  21654  ovolfiniun  21663  finiunmbl  21705  volfiniun  21708  uniioombllem3  21745  uniioombllem4  21746  mbfres2  21803  itg2splitlem  21906  itg2split  21907  itgsplit  21993  limcvallem  22026  ellimc2  22032  limccnp  22046  limccnp2  22047  limcco  22048  dvmptfsum  22127  lhop2  22167  lhop  22168  mdegcl  22220  elply2  22344  elplyd  22350  ply1term  22352  ply0  22356  plyaddlem1  22361  plymullem1  22362  plymullem  22364  mtest  22549  xrlimcnp  23042  jensen  23062  fsumharmonic  23085  chtdif  23176  lgsdir2lem3  23344  lgsquadlem2  23374  dchrisumlem2  23419  dchrisum0lem1b  23444  dchrisum0lem1  23445  pntrlog2bndlem6  23512  pntlemf  23534  eupap1  24668  shsleji  25980  shsval2i  25997  ssjo  26057  sshhococi  26156  gsumle  27449  esumsplit  27719  measun  27838  aean  27872  sxbrsigalem2  27913  subfacp1lem2a  28280  subfacp1lem3  28282  subfacp1lem5  28284  erdszelem8  28298  kur14lem7  28312  cvmliftlem10  28395  fprodsplit  28688  wfrlem16  28951  nofulllem4  29058  finixpnum  29631  mblfinlem4  29647  refssfne  29782  comppfsc  29795  topjoin  29802  tailf  29812  prdsbnd  29908  heibor1lem  29924  mzpcompact2lem  30304  eldioph2  30315  eldioph4b  30365  ttac  30598  pwssplit4  30655  isnumbasgrplem2  30673  isnumbasabl  30675  dfacbasgrp  30677  algsca  30751  algvsca  30752  fiuneneq  30775  cncfiooicclem1  31248  iblsplit  31300  fourierdlem46  31469  gsumsplit2f  32039  bnj970  33093  bnj1137  33139  bj-unrab  33584  bj-2upln1upl  33672  bj-ccinftyssccbar  33702  sspadd2  34621  pclfinN  34705  dochdmj1  36196  trclubg  36804