Theorem ssun2 3598

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 3597	. 2 |- A C_ ( A u. B )
2		uncom 3578	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3464	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3402   C_ wss 3404

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-13 2091  ax-ext 2431

This theorem depends on definitions:  df-bi 189  df-or 372  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-sb 1798  df-clab 2438  df-cleq 2444  df-clel 2447  df-nfc 2581  df-v 3047  df-un 3409  df-in 3411  df-ss 3418

This theorem is referenced by:  ssun4  3600  elun2  3602  nsspssun  3676  unv  3762  un00  3800  snsspr2  4122  snsstp3  4125  fvrn0  5887  riotassuni  6288  ovima0  6448  unexb  6591  difex2  6598  rnexg  6725  fnsuppres  6942  brtpos0  6980  wfrlem16  7051  oaabs2  7346  domunsncan  7672  mapunen  7741  ac6sfi  7815  unfir  7839  domunfican  7844  iunfi  7862  elfiun  7944  dffi3  7945  hartogslem1  8057  unwdomg  8099  unxpwdom2  8103  unxpwdom  8104  trcl  8212  unwf  8281  rankunb  8321  r0weon  8443  infxpenlem  8444  alephfplem4  8538  cda1dif  8606  cdainflem  8621  infcda  8638  cfsuc  8687  fin1a2lem10  8839  axdc3lem4  8883  ttukeylem7  8945  fpwwe2lem13  9067  canthp1lem2  9078  gchac  9106  wunrn  9154  wunex2  9163  inar1  9200  ltrelxr  9695  un0mulcl  10904  pnfxr  11412  fzdifsuc  11855  hashbclem  12615  hashf1lem1  12618  ccatfnOLD  12718  ccatrn  12733  trclublem  13059  relexprng  13109  fsumsplit  13806  o1fsum  13873  incexclem  13894  fprodsplit  14020  vdwlem5  14935  vdwlem8  14938  ramcl2  14973  ramcl2OLD  14974  srnginvl  15256  lmodvsca  15265  ipssca  15272  ipsvsca  15273  ipsip  15274  phlvsca  15282  phlip  15283  odrngtset  15308  odrngle  15309  odrngds  15310  prdssca  15354  prdsvsca  15358  prdsip  15359  prdsle  15360  prdsds  15362  prdstset  15364  prdshom  15365  prdsco  15366  imasds  15414  imassca  15420  imasvsca  15421  imasip  15422  imastset  15423  imasle  15424  imasdsOLD  15426  mreexexlemd  15550  mreexexlem2d  15551  mreexexlem3d  15552  drsdirfi  16183  ipolerval  16402  psdmrn  16453  dirge  16483  gsumzsplit  17560  gsumsplit2  17562  gsumzunsnd  17588  gsum2dlem2  17603  dprdfadd  17653  dmdprdsplit2lem  17678  dmdprdsplit2  17679  dmdprdsplit  17680  dprdsplit  17681  ablfac1eulem  17705  pgpfaclem1  17714  lspun  18210  lbsextlem2  18382  lbsextlem3  18383  lbsextlem4  18384  psrbagaddcl  18594  psrsca  18613  psrvscafval  18614  mplsubglem  18658  mplcoe5  18692  opsrtoslem2  18708  cnfldcj  18977  cnfldtset  18978  cnfldle  18979  cnfldds  18980  cnfldunif  18981  ordtbas2  20207  ordtbas  20208  ordtopn1  20210  ordtopn2  20211  leordtval2  20228  icomnfordt  20232  iooordt  20233  perfcls  20381  uncmp  20418  fiuncmp  20419  2ndcdisj2  20472  comppfsc  20547  1stckgenlem  20568  1stckgen  20569  ptbasin  20592  ptbasfi  20596  dfac14lem  20632  dfac14  20633  ptuncnv  20822  ptunhmeo  20823  ptcmpfi  20828  fbun  20855  filcon  20898  isufil2  20923  ufprim  20924  fin1aufil  20947  flimclslem  20999  flimfnfcls  21043  tmdgsum  21110  tsmsgsum  21153  tsmssplit  21166  tsmsxplem1  21167  trust  21244  prdsdsf  21382  prdsmet  21385  prdsbl  21506  cnmpt2pc  21956  rrxmetlem  22361  rrxmet  22362  rrxdstprj1  22363  ovolctb2  22445  ovolfiniun  22454  finiunmbl  22497  volfiniun  22500  uniioombllem3  22543  uniioombllem4  22544  mbfres2  22601  itg2splitlem  22706  itg2split  22707  itgsplit  22793  limcvallem  22826  ellimc2  22832  limccnp  22846  limccnp2  22847  limcco  22848  dvmptfsum  22927  lhop2  22967  lhop  22968  mdegcl  23018  elply2  23150  elplyd  23156  ply1term  23158  ply0  23162  plyaddlem1  23167  plymullem1  23168  plymullem  23170  mtest  23359  xrlimcnp  23894  jensen  23914  fsumharmonic  23937  chtdif  24085  lgsdir2lem3  24253  lgsquadlem2  24283  dchrisumlem2  24328  dchrisum0lem1b  24353  dchrisum0lem1  24354  pntrlog2bndlem6  24421  pntlemf  24443  eupap1  25704  shsleji  27023  shsval2i  27040  ssjo  27100  sshhococi  27199  gsumle  28542  esumsplit  28874  measun  29033  aean  29067  sxbrsigalem2  29108  bnj970  29758  bnj1137  29804  subfacp1lem2a  29903  subfacp1lem3  29905  subfacp1lem5  29907  erdszelem8  29921  kur14lem7  29935  cvmliftlem10  30017  mrsubvr  30149  nofulllem4  30594  refssfne  31014  topjoin  31021  tailf  31031  bj-unrab  31529  bj-2upln1upl  31618  bj-ccinftyssccbar  31660  imadifss  31928  finixpnum  31930  mblfinlem4  31980  prdsbnd  32125  heibor1lem  32141  sspadd2  33381  pclfinN  33465  dochdmj1  34958  mzpcompact2lem  35593  eldioph2  35604  eldioph4b  35654  ttac  35891  pwssplit4  35947  isnumbasgrplem2  35963  isnumbasabl  35965  dfacbasgrp  35967  algsca  36047  algvsca  36048  fiuneneq  36071  rclexi  36222  rtrclex  36224  trclubgNEW  36225  trclexi  36227  rtrclexi  36228  cnvrcl0  36232  cnvtrcl0  36233  dfrtrcl5  36236  trrelsuperrel2dg  36263  dfrcl2  36266  relexp0a  36308  relexpaddss  36310  trclimalb2  36318  frege109d  36349  frege131d  36356  iblsplit  37843  fourierdlem46  38016  sge0resplit  38248  sge0split  38251  sge0splitmpt  38253  sge0xaddlem1  38275  gsumsplit2f  40199