Theorem ssun2 3654

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 3653	. 2 |- A C_ ( A u. B )
2		uncom 3634	. 2 |- ( A u. B ) = ( B u. A )
3	1, 2	sseqtri 3521	1 |- A C_ ( B u. A )

Syntax hints:   u. cun 3459   C_ wss 3461

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-un 3466  df-in 3468  df-ss 3475

This theorem is referenced by:  ssun4  3656  elun2  3658  nsspssun  3728  unv  3812  un00  3850  snsspr2  4166  snsstp3  4169  fvrn0  5870  fnsuppresOLD  6107  riotassuniOLD  6268  ovima0  6427  unexb  6573  difex2  6580  rnexg  6705  fnsuppres  6919  brtpos0  6954  oaabs2  7286  domunsncan  7610  mapunen  7679  ac6sfi  7756  unfir  7780  domunfican  7785  iunfi  7800  elfiun  7882  dffi3  7883  hartogslem1  7959  unwdomg  8002  unxpwdom2  8006  unxpwdom  8007  trcl  8150  unwf  8219  rankunb  8259  r0weon  8381  infxpenlem  8382  alephfplem4  8479  cda1dif  8547  cdainflem  8562  infcda  8579  cfsuc  8628  fin1a2lem10  8780  axdc3lem4  8824  ttukeylem7  8886  fpwwe2lem13  9009  canthp1lem2  9020  gchac  9048  wunrn  9096  wunex2  9105  inar1  9142  ltrelxr  9637  un0mulcl  10826  pnfxr  11324  fzdifsuc  11743  hashbclem  12485  hashf1lem1  12488  ccatfnOLD  12580  ccatrn  12595  trclublem  12913  relexprng  12961  fsumsplit  13644  o1fsum  13709  incexclem  13730  fprodsplit  13852  vdwlem5  14587  vdwlem8  14590  ramcl2  14618  srnginvl  14847  lmodvsca  14856  ipssca  14863  ipsvsca  14864  ipsip  14865  phlvsca  14873  phlip  14874  odrngtset  14899  odrngle  14900  odrngds  14901  prdssca  14945  prdsvsca  14949  prdsip  14950  prdsle  14951  prdsds  14953  prdstset  14955  prdshom  14956  prdsco  14957  imasds  15002  imassca  15008  imasvsca  15009  imasip  15010  imastset  15011  imasle  15012  mreexexlemd  15133  mreexexlem2d  15134  mreexexlem3d  15135  drsdirfi  15766  ipolerval  15985  psdmrn  16036  dirge  16066  gsumzaddlemOLD  17135  gsumzsplit  17143  gsumzsplitOLD  17144  gsumsplit2  17147  gsumzunsnd  17178  gsum2dlem2  17194  gsum2dOLD  17196  dprdfadd  17255  dprdfaddOLD  17262  dmdprdsplit2lem  17289  dmdprdsplit2  17290  dmdprdsplit  17291  dprdsplit  17292  ablfac1eulem  17318  pgpfaclem1  17327  lspun  17828  lbsextlem2  18000  lbsextlem3  18001  lbsextlem4  18002  psrbagaddcl  18215  psrbagaddclOLD  18216  psrsca  18237  psrvscafval  18238  mplsubglem  18288  mplsubglemOLD  18290  mplcoe5  18326  mplcoe2OLD  18328  opsrtoslem2  18344  cnfldcj  18622  cnfldtset  18623  cnfldle  18624  cnfldds  18625  cnfldunif  18626  ordtbas2  19859  ordtbas  19860  ordtopn1  19862  ordtopn2  19863  leordtval2  19880  icomnfordt  19884  iooordt  19885  perfcls  20033  uncmp  20070  fiuncmp  20071  2ndcdisj2  20124  comppfsc  20199  1stckgenlem  20220  1stckgen  20221  ptbasin  20244  ptbasfi  20248  dfac14lem  20284  dfac14  20285  ptuncnv  20474  ptunhmeo  20475  ptcmpfi  20480  fbun  20507  filcon  20550  isufil2  20575  ufprim  20576  fin1aufil  20599  flimclslem  20651  flimfnfcls  20695  tmdgsum  20760  tsmsgsum  20803  tsmsgsumOLD  20806  tsmssplit  20820  tsmsxplem1  20821  trust  20898  prdsdsf  21036  prdsmet  21039  prdsbl  21160  cnmpt2pc  21594  rrxmetlem  22000  rrxmet  22001  rrxdstprj1  22002  ovolctb2  22069  ovolfiniun  22078  finiunmbl  22120  volfiniun  22123  uniioombllem3  22160  uniioombllem4  22161  mbfres2  22218  itg2splitlem  22321  itg2split  22322  itgsplit  22408  limcvallem  22441  ellimc2  22447  limccnp  22461  limccnp2  22462  limcco  22463  dvmptfsum  22542  lhop2  22582  lhop  22583  mdegcl  22635  elply2  22759  elplyd  22765  ply1term  22767  ply0  22771  plyaddlem1  22776  plymullem1  22777  plymullem  22779  mtest  22965  xrlimcnp  23496  jensen  23516  fsumharmonic  23539  chtdif  23630  lgsdir2lem3  23798  lgsquadlem2  23828  dchrisumlem2  23873  dchrisum0lem1b  23898  dchrisum0lem1  23899  pntrlog2bndlem6  23966  pntlemf  23988  eupap1  25178  shsleji  26486  shsval2i  26503  ssjo  26563  sshhococi  26662  gsumle  28004  esumsplit  28282  measun  28419  aean  28453  sxbrsigalem2  28494  subfacp1lem2a  28888  subfacp1lem3  28890  subfacp1lem5  28892  erdszelem8  28906  kur14lem7  28920  cvmliftlem10  29003  mrsubvr  29135  wfrlem16  29598  nofulllem4  29705  finixpnum  30278  mblfinlem4  30294  refssfne  30416  topjoin  30423  tailf  30433  prdsbnd  30529  heibor1lem  30545  mzpcompact2lem  30923  eldioph2  30934  eldioph4b  30984  ttac  31217  pwssplit4  31274  isnumbasgrplem2  31294  isnumbasabl  31296  dfacbasgrp  31298  algsca  31371  algvsca  31372  fiuneneq  31395  iblsplit  32004  fourierdlem46  32174  gsumsplit2f  33208  bnj970  34406  bnj1137  34452  bj-unrab  34895  bj-2upln1upl  34983  bj-ccinftyssccbar  35021  sspadd2  35937  pclfinN  36021  dochdmj1  37514  dfrcl2  38193  relexpaddss  38205  relexp0a  38223