Theorem ssun2 3627

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 3626	. 2 |- A C_ ( A u. B )
2		uncom 3607	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3493	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3431   C_ wss 3433

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1838  ax-10 1886  ax-11 1891  ax-12 1904  ax-13 2052  ax-ext 2398

This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-clab 2406  df-cleq 2412  df-clel 2415  df-nfc 2570  df-v 3080  df-un 3438  df-in 3440  df-ss 3447

This theorem is referenced by:  ssun4  3629  elun2  3631  nsspssun  3703  unv  3787  un00  3825  snsspr2  4144  snsstp3  4147  fvrn0  5894  riotassuni  6294  ovima0  6453  unexb  6596  difex2  6603  rnexg  6730  fnsuppres  6944  brtpos0  6979  wfrlem16  7050  oaabs2  7345  domunsncan  7669  mapunen  7738  ac6sfi  7812  unfir  7836  domunfican  7841  iunfi  7859  elfiun  7941  dffi3  7942  hartogslem1  8048  unwdomg  8090  unxpwdom2  8094  unxpwdom  8095  trcl  8202  unwf  8271  rankunb  8311  r0weon  8433  infxpenlem  8434  alephfplem4  8527  cda1dif  8595  cdainflem  8610  infcda  8627  cfsuc  8676  fin1a2lem10  8828  axdc3lem4  8872  ttukeylem7  8934  fpwwe2lem13  9056  canthp1lem2  9067  gchac  9095  wunrn  9143  wunex2  9152  inar1  9189  ltrelxr  9684  un0mulcl  10893  pnfxr  11401  fzdifsuc  11842  hashbclem  12599  hashf1lem1  12602  ccatfnOLD  12694  ccatrn  12709  trclublem  13027  relexprng  13077  fsumsplit  13773  o1fsum  13840  incexclem  13861  fprodsplit  13987  vdwlem5  14887  vdwlem8  14890  ramcl2  14925  ramcl2OLD  14926  srnginvl  15208  lmodvsca  15217  ipssca  15224  ipsvsca  15225  ipsip  15226  phlvsca  15234  phlip  15235  odrngtset  15260  odrngle  15261  odrngds  15262  prdssca  15306  prdsvsca  15310  prdsip  15311  prdsle  15312  prdsds  15314  prdstset  15316  prdshom  15317  prdsco  15318  imasds  15363  imassca  15369  imasvsca  15370  imasip  15371  imastset  15372  imasle  15373  mreexexlemd  15494  mreexexlem2d  15495  mreexexlem3d  15496  drsdirfi  16127  ipolerval  16346  psdmrn  16397  dirge  16427  gsumzsplit  17488  gsumsplit2  17490  gsumzunsnd  17516  gsum2dlem2  17531  dprdfadd  17581  dmdprdsplit2lem  17606  dmdprdsplit2  17607  dmdprdsplit  17608  dprdsplit  17609  ablfac1eulem  17633  pgpfaclem1  17642  lspun  18138  lbsextlem2  18310  lbsextlem3  18311  lbsextlem4  18312  psrbagaddcl  18522  psrsca  18541  psrvscafval  18542  mplsubglem  18586  mplcoe5  18620  opsrtoslem2  18636  cnfldcj  18905  cnfldtset  18906  cnfldle  18907  cnfldds  18908  cnfldunif  18909  ordtbas2  20131  ordtbas  20132  ordtopn1  20134  ordtopn2  20135  leordtval2  20152  icomnfordt  20156  iooordt  20157  perfcls  20305  uncmp  20342  fiuncmp  20343  2ndcdisj2  20396  comppfsc  20471  1stckgenlem  20492  1stckgen  20493  ptbasin  20516  ptbasfi  20520  dfac14lem  20556  dfac14  20557  ptuncnv  20746  ptunhmeo  20747  ptcmpfi  20752  fbun  20779  filcon  20822  isufil2  20847  ufprim  20848  fin1aufil  20871  flimclslem  20923  flimfnfcls  20967  tmdgsum  21034  tsmsgsum  21077  tsmssplit  21090  tsmsxplem1  21091  trust  21168  prdsdsf  21306  prdsmet  21309  prdsbl  21430  cnmpt2pc  21845  rrxmetlem  22247  rrxmet  22248  rrxdstprj1  22249  ovolctb2  22319  ovolfiniun  22328  finiunmbl  22371  volfiniun  22374  uniioombllem3  22417  uniioombllem4  22418  mbfres2  22475  itg2splitlem  22580  itg2split  22581  itgsplit  22667  limcvallem  22700  ellimc2  22706  limccnp  22720  limccnp2  22721  limcco  22722  dvmptfsum  22801  lhop2  22841  lhop  22842  mdegcl  22892  elply2  23015  elplyd  23021  ply1term  23023  ply0  23027  plyaddlem1  23032  plymullem1  23033  plymullem  23035  mtest  23221  xrlimcnp  23756  jensen  23776  fsumharmonic  23799  chtdif  23945  lgsdir2lem3  24113  lgsquadlem2  24143  dchrisumlem2  24188  dchrisum0lem1b  24213  dchrisum0lem1  24214  pntrlog2bndlem6  24281  pntlemf  24303  eupap1  25546  shsleji  26855  shsval2i  26872  ssjo  26932  sshhococi  27031  gsumle  28377  esumsplit  28710  measun  28869  aean  28903  sxbrsigalem2  28944  bnj970  29543  bnj1137  29589  subfacp1lem2a  29688  subfacp1lem3  29690  subfacp1lem5  29692  erdszelem8  29706  kur14lem7  29720  cvmliftlem10  29802  mrsubvr  29934  nofulllem4  30376  refssfne  30796  topjoin  30803  tailf  30813  bj-unrab  31276  bj-2upln1upl  31364  bj-ccinftyssccbar  31402  imadifss  31632  finixpnum  31634  mblfinlem4  31684  prdsbnd  31829  heibor1lem  31845  sspadd2  33090  pclfinN  33174  dochdmj1  34667  mzpcompact2lem  35302  eldioph2  35313  eldioph4b  35363  ttac  35601  pwssplit4  35657  isnumbasgrplem2  35673  isnumbasabl  35675  dfacbasgrp  35677  algsca  35750  algvsca  35751  fiuneneq  35774  trrelsuperrel2dg  35906  dfrcl2  35909  relexp0a  35951  relexpaddss  35953  trclimalb2  35961  frege109d  35992  frege131d  35999  iblsplit  37416  fourierdlem46  37588  sge0resplit  37786  sge0split  37789  sge0splitmpt  37791  gsumsplit2f  38919