Theorem ssun2 3471

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 3470	. 2 |- A C_ ( A u. B )
2		uncom 3451	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3340	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3278   C_ wss 3280

This theorem is referenced by:  ssun4  3473  elun2  3475  nsspssun  3534  unv  3615  un00  3623  snsspr2  3908  snsstp3  3911  unexb  4668  difex2  4673  rnexg  5090  fvrn0  5712  fnsuppres  5911  brtpos0  6445  riotassuni  6547  oaabs2  6847  domunsncan  7167  mapunen  7235  ac6sfi  7310  unfir  7334  domunfican  7338  iunfi  7353  elfiun  7393  dffi3  7394  hartogslem1  7467  unwdomg  7508  unxpwdom2  7512  unxpwdom  7513  trcl  7620  unwf  7692  rankunb  7732  r0weon  7850  infxpenlem  7851  alephfplem4  7944  cda1dif  8012  cdainflem  8027  infcda  8044  cfsuc  8093  fin1a2lem10  8245  axdc3lem4  8289  ttukeylem7  8351  fpwwe2lem13  8473  canthp1lem2  8484  gchac  8504  wunrn  8560  wunex2  8569  inar1  8606  ltrelxr  9095  un0mulcl  10210  pnfxr  10669  hashbclem  11656  hashf1lem1  11659  ccatfn  11696  fsumsplit  12488  o1fsum  12547  incexclem  12571  vdwlem5  13308  vdwlem8  13311  ramcl2  13339  srnginvl  13543  lmodvsca  13552  algsca  13557  algvsca  13558  phlvsca  13567  phlip  13568  odrngtset  13593  odrngle  13594  odrngds  13595  prdssca  13634  prdsvsca  13638  prdsle  13639  prdsds  13641  prdstset  13643  prdshom  13644  prdsco  13645  imasds  13694  imassca  13700  imasvsca  13701  imastset  13702  imasle  13703  mreexexlemd  13824  mreexexlem2d  13825  mreexexlem3d  13826  drsdirfi  14350  ipolerval  14537  psdmrn  14594  dirge  14637  gsumzaddlem  15481  gsumzsplit  15484  gsumsplit2  15486  gsum2d  15501  dprdfadd  15533  dmdprdsplit2lem  15558  dmdprdsplit2  15559  dmdprdsplit  15560  dprdsplit  15561  ablfac1eulem  15585  pgpfaclem1  15594  lspun  16018  lbsextlem2  16186  lbsextlem3  16187  lbsextlem4  16188  psrbagaddcl  16390  psrsca  16408  psrvscafval  16409  mplsubglem  16453  mplcoe2  16485  opsrtoslem2  16500  cnfldcj  16665  cnfldtset  16666  cnfldle  16667  cnfldds  16668  cnfldunif  16669  ordtbas2  17209  ordtbas  17210  ordtopn1  17212  ordtopn2  17213  leordtval2  17230  icomnfordt  17234  iooordt  17235  perfcls  17383  uncmp  17420  fiuncmp  17421  2ndcdisj2  17473  1stckgenlem  17538  1stckgen  17539  ptbasin  17562  ptbasfi  17566  dfac14lem  17602  dfac14  17603  ptuncnv  17792  ptunhmeo  17793  ptcmpfi  17798  fbun  17825  filcon  17868  isufil2  17893  ufprim  17894  fin1aufil  17917  flimclslem  17969  flimfnfcls  18013  tmdgsum  18078  tsmsgsum  18121  tsmssplit  18134  tsmsxplem1  18135  trust  18212  prdsdsf  18350  prdsmet  18353  prdsbl  18474  cnmpt2pc  18906  ovolctb2  19341  ovolfiniun  19350  finiunmbl  19391  volfiniun  19394  uniioombllem3  19430  uniioombllem4  19431  mbfres2  19490  itg2splitlem  19593  itg2split  19594  itgsplit  19680  limcvallem  19711  ellimc2  19717  limccnp  19731  limccnp2  19732  limcco  19733  dvmptfsum  19812  lhop2  19852  lhop  19853  mdegcl  19945  elply2  20068  elplyd  20074  ply1term  20076  ply0  20080  plyaddlem1  20085  plymullem1  20086  plymullem  20088  mtest  20273  xrlimcnp  20760  jensen  20780  fsumharmonic  20803  chtdif  20894  lgsdir2lem3  21062  lgsquadlem2  21092  dchrisumlem2  21137  dchrisum0lem1b  21162  dchrisum0lem1  21163  pntrlog2bndlem6  21230  pntlemf  21252  eupap1  21651  shsleji  22825  shsval2i  22842  ssjo  22902  sshhococi  23001  esumsplit  24400  measun  24518  aean  24548  sxbrsigalem2  24589  subfacp1lem2a  24819  subfacp1lem3  24821  subfacp1lem5  24823  erdszelem8  24837  kur14lem7  24851  cvmliftlem10  24934  fprodsplit  25242  wfrlem14  25483  wfrlem16  25485  nofulllem4  25573  mblfinlem3  26145  refssfne  26264  comppfsc  26277  topjoin  26284  tailf  26294  prdsbnd  26392  heibor1lem  26408  mzpcompact2lem  26698  eldioph2  26710  eldioph4b  26762  ttac  26997  pwssplit4  27059  isnumbasgrplem2  27137  isnumbasabl  27139  dfacbasgrp  27141  fiuneneq  27381  bnj970  29024  bnj1137  29070  sspadd2  30298  pclfinN  30382  dochdmj1  31873

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385

This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-clab 2391  df-cleq 2397  df-clel 2400  df-nfc 2529  df-v 2918  df-un 3285  df-in 3287  df-ss 3294