Theorem ssun2 3777

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 3776	. 2 |- A C_ ( A u. B )
2		uncom 3757	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3637	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3572   C_ wss 3574

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-un 3579  df-in 3581  df-ss 3588

This theorem is referenced by:  ssun4  3779  elun2  3781  nsspssun  3857  unv  3971  un00  4011  snsspr2  4346  snsstp3  4349  fvrn0  6216  riotassuni  6648  ovima0  6813  unexb  6958  difex2  6969  rnexg  7098  fnsuppres  7322  brtpos0  7359  wfrlem16  7430  oaabs2  7725  domunsncan  8060  mapunen  8129  ac6sfi  8204  unfir  8228  domunfican  8233  iunfi  8254  elfiun  8336  dffi3  8337  hartogslem1  8447  unwdomg  8489  unxpwdom2  8493  unxpwdom  8494  trcl  8604  unwf  8673  rankunb  8713  r0weon  8835  infxpenlem  8836  alephfplem4  8930  cda1dif  8998  cdainflem  9013  infcda  9030  cfsuc  9079  fin1a2lem10  9231  axdc3lem4  9275  ttukeylem7  9337  fpwwe2lem13  9464  canthp1lem2  9475  gchac  9503  wunrn  9551  wunex2  9560  inar1  9597  pnfxr  10092  ltrelxr  10099  un0mulcl  11327  fzdifsuc  12400  hashbclem  13236  hashf1lem1  13239  ccatrn  13372  trclublem  13734  relexprng  13786  fsumsplit  14471  o1fsum  14545  incexclem  14568  fprodsplit  14696  vdwlem5  15689  vdwlem8  15692  ramcl2  15720  srnginvl  16012  lmodvsca  16021  ipssca  16028  ipsvsca  16029  ipsip  16030  phlvsca  16038  phlip  16039  odrngtset  16070  odrngle  16071  odrngds  16072  prdssca  16116  prdsvsca  16120  prdsip  16121  prdsle  16122  prdsds  16124  prdstset  16126  prdshom  16127  prdsco  16128  imasds  16173  imassca  16179  imasvsca  16180  imasip  16181  imastset  16182  imasle  16183  mreexexlemd  16304  mreexexlem2d  16305  mreexexlem3d  16306  drsdirfi  16938  ipolerval  17156  psdmrn  17207  dirge  17237  gsumzsplit  18327  gsumsplit2  18329  gsumzunsnd  18355  gsum2dlem2  18370  dprdfadd  18419  dmdprdsplit2lem  18444  dmdprdsplit2  18445  dmdprdsplit  18446  dprdsplit  18447  ablfac1eulem  18471  pgpfaclem1  18480  lspun  18987  lbsextlem2  19159  lbsextlem3  19160  lbsextlem4  19161  psrbagaddcl  19370  psrsca  19389  psrvscafval  19390  mplsubglem  19434  mplcoe5  19468  opsrtoslem2  19485  cnfldcj  19753  cnfldtset  19754  cnfldle  19755  cnfldds  19756  cnfldunif  19757  ordtbas2  20995  ordtbas  20996  ordtopn1  20998  ordtopn2  20999  leordtval2  21016  icomnfordt  21020  iooordt  21021  perfcls  21169  uncmp  21206  fiuncmp  21207  2ndcdisj2  21260  comppfsc  21335  1stckgenlem  21356  1stckgen  21357  ptbasin  21380  ptbasfi  21384  dfac14lem  21420  dfac14  21421  ptuncnv  21610  ptunhmeo  21611  ptcmpfi  21616  fbun  21644  filconn  21687  isufil2  21712  ufprim  21713  fin1aufil  21736  flimclslem  21788  flimfnfcls  21832  tmdgsum  21899  tsmsgsum  21942  tsmssplit  21955  tsmsxplem1  21956  trust  22033  prdsdsf  22172  prdsmet  22175  prdsbl  22296  cnmpt2pc  22727  rrxmetlem  23190  rrxmet  23191  rrxdstprj1  23192  ovolctb2  23260  ovolfiniun  23269  finiunmbl  23312  volfiniun  23315  uniioombllem3  23353  uniioombllem4  23354  mbfres2  23412  itg2splitlem  23515  itg2split  23516  itgsplit  23602  limcvallem  23635  ellimc2  23641  limccnp  23655  limccnp2  23656  limcco  23657  dvmptfsum  23738  lhop2  23778  lhop  23779  mdegcl  23829  elply2  23952  elplyd  23958  ply1term  23960  ply0  23964  plyaddlem1  23969  plymullem1  23970  plymullem  23972  mtest  24158  xrlimcnp  24695  jensen  24715  fsumharmonic  24738  chtdif  24884  lgsdir2lem3  25052  lgsquadlem2  25106  dchrisumlem2  25179  dchrisum0lem1b  25204  dchrisum0lem1  25205  pntrlog2bndlem6  25272  pntlemf  25294  shsleji  28229  shsval2i  28246  ssjo  28306  sshhococi  28405  gsumle  29779  esumsplit  30115  measun  30274  aean  30307  sxbrsigalem2  30348  bnj970  31017  bnj1137  31063  subfacp1lem2a  31162  subfacp1lem3  31164  subfacp1lem5  31166  erdszelem8  31180  kur14lem7  31194  cvmliftlem10  31276  mrsubvr  31408  noetalem3  31865  refssfne  32353  topjoin  32360  tailf  32370  bj-unrab  32922  bj-2upln1upl  33012  bj-ccinftyssccbar  33105  imadifss  33384  finixpnum  33394  matunitlindflem1  33405  mblfinlem4  33449  prdsbnd  33592  heibor1lem  33608  sspadd2  35102  pclfinN  35186  dochdmj1  36679  mzpcompact2lem  37314  eldioph2  37325  eldioph4b  37375  ttac  37603  pwssplit4  37659  isnumbasgrplem2  37674  isnumbasabl  37676  dfacbasgrp  37678  algsca  37751  algvsca  37752  fiuneneq  37775  rclexi  37922  rtrclex  37924  trclubgNEW  37925  trclexi  37927  rtrclexi  37928  cnvrcl0  37932  cnvtrcl0  37933  dfrtrcl5  37936  trrelsuperrel2dg  37963  dfrcl2  37966  relexp0a  38008  relexpaddss  38010  trclimalb2  38018  frege109d  38049  frege131d  38056  isotone1  38346  iblsplit  40182  fourierdlem46  40369  sge0resplit  40623  sge0split  40626  sge0splitmpt  40628  sge0xaddlem1  40650  sbgoldbo  41675  gsumsplit2f  42143  setrec1  42438  elpglem2  42455