Theorem ssun2 4188

Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)

Assertion

Ref	Expression
ssun2	⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Proof of Theorem ssun2

Step	Hyp	Ref	Expression
1		ssun1 4187	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4167	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4031	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3960   ⊆ wss 3962

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-un 3967  df-ss 3979

This theorem is referenced by:  ssun4  4190  elun2  4192  nsspssun  4273  unv  4404  un00  4450  pwunss  4622  snsspr2  4819  snsstp3  4822  fvrn0  6936  riotassuni  7427  ovima0  7611  unexb  7765  unexbOLD  7766  difex2  7778  rnexg  7924  xpord2indlem  8170  xpord3inddlem  8177  fnsuppres  8214  brtpos0  8256  frrlem14  8322  wfrlem16OLD  8362  oaabs2  8685  domunsncan  9110  mapunen  9184  ac6sfi  9317  unfir  9343  domunfican  9358  iunfi  9380  elfiun  9467  dffi3  9468  hartogslem1  9579  unwdomg  9621  unxpwdom2  9625  unxpwdom  9626  trcl  9765  unwf  9847  rankunb  9887  r0weon  10049  infxpenlem  10050  alephfplem4  10144  dju1dif  10210  cdainflem  10225  infdju  10244  cfsuc  10294  fin1a2lem10  10446  axdc3lem4  10490  ttukeylem7  10552  fpwwe2lem12  10679  canthp1lem2  10690  gchac  10718  wunrn  10766  wunex2  10775  inar1  10812  pnfxr  11312  ltrelxr  11319  un0mulcl  12557  fzdifsuc  13620  seqexw  14054  hashbclem  14487  hashf1lem1  14490  ccatrn  14623  trclublem  15030  relexprng  15081  fsumsplit  15773  o1fsum  15845  incexclem  15868  fprodsplit  15998  vdwlem5  17018  vdwlem8  17021  ramcl2  17049  srnginvl  17358  lmodvsca  17374  ipssca  17385  ipsvsca  17386  ipsip  17387  phlvsca  17395  phlip  17396  odrngtset  17452  odrngle  17453  odrngds  17454  prdssca  17502  prdsvsca  17506  prdsip  17507  prdsle  17508  prdsds  17510  prdstset  17512  prdshom  17513  prdsco  17514  imasds  17559  imassca  17565  imasvsca  17566  imasip  17567  imastset  17568  imasle  17569  mreexexlemd  17688  mreexexlem2d  17689  mreexexlem3d  17690  drsdirfi  18362  ipolerval  18589  psdmrn  18630  dirge  18660  grpinvfval  19008  mulgfval  19099  gsumzsplit  19959  gsumsplit2  19961  gsumzunsnd  19988  gsum2dlem2  20003  dprdfadd  20054  dmdprdsplit2lem  20079  dmdprdsplit2  20080  dmdprdsplit  20081  dprdsplit  20082  ablfac1eulem  20106  pgpfaclem1  20115  lspun  21002  lbsextlem2  21178  lbsextlem3  21179  lbsextlem4  21180  cnfldcj  21390  cnfldtset  21391  cnfldle  21392  cnfldds  21393  cnfldunif  21394  cnfldcjOLD  21403  cnfldtsetOLD  21404  cnfldleOLD  21405  cnflddsOLD  21406  cnfldunifOLD  21407  psrsca  21984  psrvscafval  21985  mplsubglem  22036  mplcoe5  22075  opsrtoslem2  22097  ordtbas2  23214  ordtbas  23215  ordtopn1  23217  ordtopn2  23218  leordtval2  23235  icomnfordt  23239  iooordt  23240  perfcls  23388  uncmp  23426  fiuncmp  23427  2ndcdisj2  23480  comppfsc  23555  1stckgenlem  23576  1stckgen  23577  ptbasin  23600  ptbasfi  23604  dfac14lem  23640  dfac14  23641  ptuncnv  23830  ptunhmeo  23831  ptcmpfi  23836  fbun  23863  filconn  23906  isufil2  23931  ufprim  23932  fin1aufil  23955  flimclslem  24007  flimfnfcls  24051  tmdgsum  24118  tsmsgsum  24162  tsmssplit  24175  tsmsxplem1  24176  trust  24253  prdsdsf  24392  prdsmet  24395  prdsbl  24519  cnmpopc  24968  rrxmetlem  25454  rrxmet  25455  rrxdstprj1  25456  ovolctb2  25540  ovolfiniun  25549  finiunmbl  25592  volfiniun  25595  uniioombllem3  25633  uniioombllem4  25634  mbfres2  25693  itg2splitlem  25797  itg2split  25798  itgsplit  25885  limcvallem  25920  ellimc2  25926  limccnp  25940  limccnp2  25941  limcco  25942  dvmptfsum  26027  lhop2  26068  lhop  26069  mdegcl  26122  elply2  26249  elplyd  26255  ply1term  26257  ply0  26261  plyaddlem1  26266  plymullem1  26267  plymullem  26269  mtest  26461  xrlimcnp  27025  jensen  27046  fsumharmonic  27069  chtdif  27215  lgsdir2lem3  27385  lgsquadlem2  27439  dchrisumlem2  27548  dchrisum0lem1b  27573  dchrisum0lem1  27574  pntrlog2bndlem6  27641  pntlemf  27663  nosupinfsep  27791  noetasuplem4  27795  noetalem1  27800  cofcutrtime  27975  addsuniflem  28048  addsbday  28064  negsval  28071  mulsproplem12  28167  mulsproplem13  28168  mulsproplem14  28169  mulsuniflem  28189  mulsass  28206  precsexlem10  28254  shsleji  31398  shsval2i  31415  ssjo  31475  sshhococi  31574  gsumle  33083  symgcom  33085  elrspunsn  33436  idlsrgtset  33515  rtelextdg2  33732  esumsplit  34033  measun  34191  aean  34224  sxbrsigalem2  34267  bnj970  34939  bnj1137  34987  subfacp1lem2a  35164  subfacp1lem3  35166  subfacp1lem5  35168  erdszelem8  35182  kur14lem7  35196  cvmliftlem10  35278  mrsubvr  35495  refssfne  36340  topjoin  36347  tailf  36357  bj-unrab  36908  bj-2upln1upl  37006  bj-ccinftyssccbar  37200  imadifss  37581  finixpnum  37591  matunitlindflem1  37602  mblfinlem4  37646  prdsbnd  37779  heibor1lem  37795  sspadd2  39798  pclfinN  39882  dochdmj1  41372  mzpcompact2lem  42738  eldioph2  42749  eldioph4b  42798  ttac  43024  pwssplit4  43077  isnumbasgrplem2  43092  isnumbasabl  43094  dfacbasgrp  43096  algsca  43165  algvsca  43166  fiuneneq  43180  tfsconcatrnss12  43338  rclexi  43604  rtrclex  43606  trclubgNEW  43607  trclexi  43609  rtrclexi  43610  cnvrcl0  43614  cnvtrcl0  43615  dfrtrcl5  43618  trrelsuperrel2dg  43660  dfrcl2  43663  relexp0a  43705  relexpaddss  43707  trclimalb2  43715  frege109d  43746  frege131d  43753  isotone1  44037  grumnudlem  44280  rnwf  44940  iblsplit  45921  fourierdlem46  46107  sge0resplit  46361  sge0split  46364  sge0splitmpt  46366  sge0xaddlem1  46388  sbgoldbo  47711  dfnbgrss  47775  gsumsplit2f  48023  setrec1  48921  elpglem2  48942