Theorem ssun2 3650

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 3649	. 2 |- A C_ ( A u. B )
2		uncom 3630	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3518	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3456   C_ wss 3458

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1603  ax-4 1616  ax-5 1689  ax-6 1732  ax-7 1774  ax-10 1821  ax-11 1826  ax-12 1838  ax-13 1983  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1384  df-ex 1598  df-nf 1602  df-sb 1725  df-clab 2427  df-cleq 2433  df-clel 2436  df-nfc 2591  df-v 3095  df-un 3463  df-in 3465  df-ss 3472

This theorem is referenced by:  ssun4  3652  elun2  3654  nsspssun  3713  unv  3795  un00  3844  snsspr2  4161  snsstp3  4164  fvrn0  5874  fnsuppresOLD  6112  riotassuniOLD  6275  ovima0  6435  unexb  6581  difex2  6588  rnexg  6713  fnsuppres  6925  brtpos0  6960  oaabs2  7292  domunsncan  7615  mapunen  7684  ac6sfi  7762  unfir  7786  domunfican  7791  iunfi  7806  elfiun  7888  dffi3  7889  hartogslem1  7965  unwdomg  8008  unxpwdom2  8012  unxpwdom  8013  trcl  8157  unwf  8226  rankunb  8266  r0weon  8388  infxpenlem  8389  alephfplem4  8486  cda1dif  8554  cdainflem  8569  infcda  8586  cfsuc  8635  fin1a2lem10  8787  axdc3lem4  8831  ttukeylem7  8893  fpwwe2lem13  9018  canthp1lem2  9029  gchac  9057  wunrn  9105  wunex2  9114  inar1  9151  ltrelxr  9646  un0mulcl  10831  pnfxr  11325  fzdifsuc  11743  hashbclem  12475  hashf1lem1  12478  ccatfn  12565  ccatrn  12580  fsumsplit  13536  o1fsum  13601  incexclem  13622  vdwlem5  14375  vdwlem8  14378  ramcl2  14406  srnginvl  14628  lmodvsca  14637  ipssca  14644  ipsvsca  14645  ipsip  14646  phlvsca  14654  phlip  14655  odrngtset  14680  odrngle  14681  odrngds  14682  prdssca  14725  prdsvsca  14729  prdsip  14730  prdsle  14731  prdsds  14733  prdstset  14735  prdshom  14736  prdsco  14737  imasds  14782  imassca  14788  imasvsca  14789  imasip  14790  imastset  14791  imasle  14792  mreexexlemd  14913  mreexexlem2d  14914  mreexexlem3d  14915  drsdirfi  15436  ipolerval  15655  psdmrn  15706  dirge  15736  gsumzaddlemOLD  16805  gsumzsplit  16813  gsumzsplitOLD  16814  gsumsplit2  16817  gsumsplit2OLD  16818  gsumzunsnd  16851  gsum2dlem2  16867  gsum2dOLD  16869  dprdfadd  16928  dprdfaddOLD  16935  dmdprdsplit2lem  16962  dmdprdsplit2  16963  dmdprdsplit  16964  dprdsplit  16965  ablfac1eulem  16991  pgpfaclem1  17000  lspun  17501  lbsextlem2  17673  lbsextlem3  17674  lbsextlem4  17675  psrbagaddcl  17888  psrbagaddclOLD  17889  psrsca  17910  psrvscafval  17911  mplsubglem  17961  mplsubglemOLD  17963  mplcoe5  17999  mplcoe2OLD  18001  opsrtoslem2  18017  cnfldcj  18295  cnfldtset  18296  cnfldle  18297  cnfldds  18298  cnfldunif  18299  ordtbas2  19558  ordtbas  19559  ordtopn1  19561  ordtopn2  19562  leordtval2  19579  icomnfordt  19583  iooordt  19584  perfcls  19732  uncmp  19769  fiuncmp  19770  2ndcdisj2  19824  comppfsc  19899  1stckgenlem  19920  1stckgen  19921  ptbasin  19944  ptbasfi  19948  dfac14lem  19984  dfac14  19985  ptuncnv  20174  ptunhmeo  20175  ptcmpfi  20180  fbun  20207  filcon  20250  isufil2  20275  ufprim  20276  fin1aufil  20299  flimclslem  20351  flimfnfcls  20395  tmdgsum  20460  tsmsgsum  20503  tsmsgsumOLD  20506  tsmssplit  20520  tsmsxplem1  20521  trust  20598  prdsdsf  20736  prdsmet  20739  prdsbl  20860  cnmpt2pc  21294  rrxmetlem  21700  rrxmet  21701  rrxdstprj1  21702  ovolctb2  21769  ovolfiniun  21778  finiunmbl  21820  volfiniun  21823  uniioombllem3  21860  uniioombllem4  21861  mbfres2  21918  itg2splitlem  22021  itg2split  22022  itgsplit  22108  limcvallem  22141  ellimc2  22147  limccnp  22161  limccnp2  22162  limcco  22163  dvmptfsum  22242  lhop2  22282  lhop  22283  mdegcl  22335  elply2  22459  elplyd  22465  ply1term  22467  ply0  22471  plyaddlem1  22476  plymullem1  22477  plymullem  22479  mtest  22664  xrlimcnp  23163  jensen  23183  fsumharmonic  23206  chtdif  23297  lgsdir2lem3  23465  lgsquadlem2  23495  dchrisumlem2  23540  dchrisum0lem1b  23565  dchrisum0lem1  23566  pntrlog2bndlem6  23633  pntlemf  23655  eupap1  24841  shsleji  26153  shsval2i  26170  ssjo  26230  sshhococi  26329  gsumle  27636  esumsplit  27929  measun  28048  aean  28082  sxbrsigalem2  28123  subfacp1lem2a  28490  subfacp1lem3  28492  subfacp1lem5  28494  erdszelem8  28508  kur14lem7  28522  cvmliftlem10  28605  mrsubvr  28737  fprodsplit  29063  wfrlem16  29326  nofulllem4  29433  finixpnum  30006  mblfinlem4  30022  refssfne  30144  topjoin  30151  tailf  30161  prdsbnd  30257  heibor1lem  30273  mzpcompact2lem  30652  eldioph2  30663  eldioph4b  30713  ttac  30946  pwssplit4  31003  isnumbasgrplem2  31021  isnumbasabl  31023  dfacbasgrp  31025  algsca  31099  algvsca  31100  fiuneneq  31123  iblsplit  31651  fourierdlem46  31820  gsumsplit2f  32662  bnj970  33712  bnj1137  33758  bj-unrab  34206  bj-2upln1upl  34294  bj-ccinftyssccbar  34323  sspadd2  35242  pclfinN  35326  dochdmj1  36819  trclubg  37440