Theorem ssun2 3517

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 3516	. 2 |- A C_ ( A u. B )
2		uncom 3497	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3385	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3323   C_ wss 3325

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1713  ax-7 1733  ax-10 1780  ax-11 1785  ax-12 1797  ax-13 1948  ax-ext 2422

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1367  df-ex 1592  df-nf 1595  df-sb 1706  df-clab 2428  df-cleq 2434  df-clel 2437  df-nfc 2566  df-v 2972  df-un 3330  df-in 3332  df-ss 3339

This theorem is referenced by:  ssun4  3519  elun2  3521  nsspssun  3580  unv  3662  un00  3711  snsspr2  4020  snsstp3  4023  fvrn0  5709  fnsuppresOLD  5935  riotassuniOLD  6088  ovima0  6241  unexb  6379  difex2  6382  rnexg  6509  fnsuppres  6715  brtpos0  6751  oaabs2  7080  domunsncan  7407  mapunen  7476  ac6sfi  7552  unfir  7576  domunfican  7580  iunfi  7595  elfiun  7676  dffi3  7677  hartogslem1  7752  unwdomg  7795  unxpwdom2  7799  unxpwdom  7800  trcl  7944  unwf  8013  rankunb  8053  r0weon  8175  infxpenlem  8176  alephfplem4  8273  cda1dif  8341  cdainflem  8356  infcda  8373  cfsuc  8422  fin1a2lem10  8574  axdc3lem4  8618  ttukeylem7  8680  fpwwe2lem13  8805  canthp1lem2  8816  gchac  8844  wunrn  8892  wunex2  8901  inar1  8938  ltrelxr  9434  un0mulcl  10610  pnfxr  11088  fzdifsuc  11512  hashbclem  12201  hashf1lem1  12204  ccatfn  12268  fsumsplit  13212  o1fsum  13272  incexclem  13295  vdwlem5  14042  vdwlem8  14045  ramcl2  14073  srnginvl  14293  lmodvsca  14302  ipssca  14309  ipsvsca  14310  ipsip  14311  phlvsca  14319  phlip  14320  odrngtset  14345  odrngle  14346  odrngds  14347  prdssca  14390  prdsvsca  14394  prdsip  14395  prdsle  14396  prdsds  14398  prdstset  14400  prdshom  14401  prdsco  14402  imasds  14447  imassca  14453  imasvsca  14454  imasip  14455  imastset  14456  imasle  14457  mreexexlemd  14578  mreexexlem2d  14579  mreexexlem3d  14580  drsdirfi  15104  ipolerval  15322  psdmrn  15373  dirge  15403  gsumzaddlemOLD  16403  gsumzsplit  16411  gsumzsplitOLD  16412  gsumsplit2  16415  gsumsplit2OLD  16416  gsum2dlem2  16452  gsum2dOLD  16454  dprdfadd  16500  dprdfaddOLD  16507  dmdprdsplit2lem  16534  dmdprdsplit2  16535  dmdprdsplit  16536  dprdsplit  16537  ablfac1eulem  16563  pgpfaclem1  16572  lspun  17046  lbsextlem2  17218  lbsextlem3  17219  lbsextlem4  17220  psrbagaddcl  17416  psrbagaddclOLD  17417  psrsca  17438  psrvscafval  17439  mplsubglem  17488  mplsubglemOLD  17490  mplcoe2  17525  mplcoe2OLD  17526  opsrtoslem2  17542  cnfldcj  17784  cnfldtset  17785  cnfldle  17786  cnfldds  17787  cnfldunif  17788  ordtbas2  18754  ordtbas  18755  ordtopn1  18757  ordtopn2  18758  leordtval2  18775  icomnfordt  18779  iooordt  18780  perfcls  18928  uncmp  18965  fiuncmp  18966  2ndcdisj2  19020  1stckgenlem  19085  1stckgen  19086  ptbasin  19109  ptbasfi  19113  dfac14lem  19149  dfac14  19150  ptuncnv  19339  ptunhmeo  19340  ptcmpfi  19345  fbun  19372  filcon  19415  isufil2  19440  ufprim  19441  fin1aufil  19464  flimclslem  19516  flimfnfcls  19560  tmdgsum  19625  tsmsgsum  19668  tsmsgsumOLD  19671  tsmssplit  19685  tsmsxplem1  19686  trust  19763  prdsdsf  19901  prdsmet  19904  prdsbl  20025  cnmpt2pc  20459  rrxmetlem  20865  rrxmet  20866  rrxdstprj1  20867  ovolctb2  20934  ovolfiniun  20943  finiunmbl  20984  volfiniun  20987  uniioombllem3  21024  uniioombllem4  21025  mbfres2  21082  itg2splitlem  21185  itg2split  21186  itgsplit  21272  limcvallem  21305  ellimc2  21311  limccnp  21325  limccnp2  21326  limcco  21327  dvmptfsum  21406  lhop2  21446  lhop  21447  mdegcl  21499  elply2  21623  elplyd  21629  ply1term  21631  ply0  21635  plyaddlem1  21640  plymullem1  21641  plymullem  21643  mtest  21828  xrlimcnp  22321  jensen  22341  fsumharmonic  22364  chtdif  22455  lgsdir2lem3  22623  lgsquadlem2  22653  dchrisumlem2  22698  dchrisum0lem1b  22723  dchrisum0lem1  22724  pntrlog2bndlem6  22791  pntlemf  22813  eupap1  23532  shsleji  24708  shsval2i  24725  ssjo  24785  sshhococi  24884  gsumle  26181  gsummptun  26183  gsumvsca1  26186  gsumvsca2  26187  esumsplit  26442  measun  26561  aean  26596  sxbrsigalem2  26637  subfacp1lem2a  26998  subfacp1lem3  27000  subfacp1lem5  27002  erdszelem8  27016  kur14lem7  27030  cvmliftlem10  27113  fprodsplit  27405  wfrlem16  27668  nofulllem4  27775  finixpnum  28339  mblfinlem4  28356  refssfne  28491  comppfsc  28504  topjoin  28511  tailf  28521  prdsbnd  28617  heibor1lem  28633  mzpcompact2lem  29013  eldioph2  29025  eldioph4b  29075  ttac  29310  pwssplit4  29367  isnumbasgrplem2  29385  isnumbasabl  29387  dfacbasgrp  29389  algsca  29463  algvsca  29464  fiuneneq  29487  gsumsplit2f  30681  bnj970  31774  bnj1137  31820  bj-unrab  32162  bj-2upln1upl  32247  bj-ccinftyssccbar  32270  sspadd2  33182  pclfinN  33266  dochdmj1  34757