Theorem ssun2 4129

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 4128	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4108	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3983	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3900   ⊆ wss 3902

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-un 3907  df-ss 3919

This theorem is referenced by:  ssun4  4131  elun2  4133  nsspssun  4218  unv  4349  un00  4395  pwunss  4568  snsspr2  4767  snsstp3  4770  fvrn0  6850  riotassuni  7343  ovima0  7525  unexb  7680  unexbOLD  7681  difex2  7693  rnexg  7832  xpord2indlem  8077  xpord3inddlem  8084  fnsuppres  8121  brtpos0  8163  frrlem14  8229  oaabs2  8564  domunsncan  8990  mapunen  9059  ac6sfi  9168  unfir  9192  domunfican  9206  iunfi  9227  elfiun  9314  dffi3  9315  hartogslem1  9428  unwdomg  9470  unxpwdom2  9474  unxpwdom  9475  trcl  9618  unwf  9703  rankunb  9743  r0weon  9903  infxpenlem  9904  alephfplem4  9998  dju1dif  10064  cdainflem  10079  infdju  10098  cfsuc  10148  fin1a2lem10  10300  axdc3lem4  10344  ttukeylem7  10406  fpwwe2lem12  10533  canthp1lem2  10544  gchac  10572  wunrn  10620  wunex2  10629  inar1  10666  pnfxr  11166  ltrelxr  11173  un0mulcl  12415  fzdifsuc  13484  seqexw  13924  hashbclem  14359  hashf1lem1  14362  ccatrn  14497  trclublem  14902  relexprng  14953  fsumsplit  15648  o1fsum  15720  incexclem  15743  fprodsplit  15873  vdwlem5  16897  vdwlem8  16900  ramcl2  16928  srnginvl  17217  lmodvsca  17233  ipssca  17244  ipsvsca  17245  ipsip  17246  phlvsca  17254  phlip  17255  odrngtset  17311  odrngle  17312  odrngds  17313  prdssca  17360  prdsvsca  17364  prdsip  17365  prdsle  17366  prdsds  17368  prdstset  17370  prdshom  17371  prdsco  17372  imasds  17417  imassca  17423  imasvsca  17424  imasip  17425  imastset  17426  imasle  17427  mreexexlemd  17550  mreexexlem2d  17551  mreexexlem3d  17552  drsdirfi  18211  ipolerval  18438  psdmrn  18479  dirge  18509  grpinvfval  18891  mulgfval  18982  gsumzsplit  19840  gsumsplit2  19842  gsumzunsnd  19869  gsum2dlem2  19884  dprdfadd  19935  dmdprdsplit2lem  19960  dmdprdsplit2  19961  dmdprdsplit  19962  dprdsplit  19963  ablfac1eulem  19987  pgpfaclem1  19996  gsumle  20058  lspun  20921  lbsextlem2  21097  lbsextlem3  21098  lbsextlem4  21099  cnfldcj  21301  cnfldtset  21302  cnfldle  21303  cnfldds  21304  cnfldunif  21305  cnfldcjOLD  21314  cnfldtsetOLD  21315  cnfldleOLD  21316  cnflddsOLD  21317  cnfldunifOLD  21318  psrsca  21885  psrvscafval  21886  mplsubglem  21937  mplcoe5  21976  opsrtoslem2  21992  ordtbas2  23107  ordtbas  23108  ordtopn1  23110  ordtopn2  23111  leordtval2  23128  icomnfordt  23132  iooordt  23133  perfcls  23281  uncmp  23319  fiuncmp  23320  2ndcdisj2  23373  comppfsc  23448  1stckgenlem  23469  1stckgen  23470  ptbasin  23493  ptbasfi  23497  dfac14lem  23533  dfac14  23534  ptuncnv  23723  ptunhmeo  23724  ptcmpfi  23729  fbun  23756  filconn  23799  isufil2  23824  ufprim  23825  fin1aufil  23848  flimclslem  23900  flimfnfcls  23944  tmdgsum  24011  tsmsgsum  24055  tsmssplit  24068  tsmsxplem1  24069  trust  24145  prdsdsf  24283  prdsmet  24286  prdsbl  24407  cnmpopc  24850  rrxmetlem  25335  rrxmet  25336  rrxdstprj1  25337  ovolctb2  25421  ovolfiniun  25430  finiunmbl  25473  volfiniun  25476  uniioombllem3  25514  uniioombllem4  25515  mbfres2  25574  itg2splitlem  25677  itg2split  25678  itgsplit  25765  limcvallem  25800  ellimc2  25806  limccnp  25820  limccnp2  25821  limcco  25822  dvmptfsum  25907  lhop2  25948  lhop  25949  mdegcl  26002  elply2  26129  elplyd  26135  ply1term  26137  ply0  26141  plyaddlem1  26146  plymullem1  26147  plymullem  26149  mtest  26341  xrlimcnp  26906  jensen  26927  fsumharmonic  26950  chtdif  27096  lgsdir2lem3  27266  lgsquadlem2  27320  dchrisumlem2  27429  dchrisum0lem1b  27454  dchrisum0lem1  27455  pntrlog2bndlem6  27522  pntlemf  27544  nosupinfsep  27672  noetasuplem4  27676  noetalem1  27681  cofcutrtime  27872  addsuniflem  27945  addsbday  27961  negsval  27968  mulsproplem12  28067  mulsproplem13  28068  mulsproplem14  28069  mulsuniflem  28089  mulsass  28106  precsexlem10  28155  bdayn0p1  28295  shsleji  31348  shsval2i  31365  ssjo  31425  sshhococi  31524  symgcom  33050  elrgspnsubrunlem1  33212  elrgspnsubrunlem2  33213  elrspunsn  33392  idlsrgtset  33471  rtelextdg2  33738  constrextdg2lem  33759  esumsplit  34064  measun  34222  aean  34255  sxbrsigalem2  34297  bnj970  34957  bnj1137  35005  subfacp1lem2a  35222  subfacp1lem3  35224  subfacp1lem5  35226  erdszelem8  35240  kur14lem7  35254  cvmliftlem10  35336  mrsubvr  35553  refssfne  36398  topjoin  36405  tailf  36415  bj-unrab  36966  bj-2upln1upl  37064  bj-ccinftyssccbar  37258  imadifss  37641  finixpnum  37651  matunitlindflem1  37662  mblfinlem4  37706  prdsbnd  37839  heibor1lem  37855  sspadd2  39861  pclfinN  39945  dochdmj1  41435  mzpcompact2lem  42790  eldioph2  42801  eldioph4b  42850  ttac  43075  pwssplit4  43128  isnumbasgrplem2  43143  isnumbasabl  43145  dfacbasgrp  43147  algsca  43216  algvsca  43217  fiuneneq  43231  tfsconcatrnss12  43388  rclexi  43654  rtrclex  43656  trclubgNEW  43657  trclexi  43659  rtrclexi  43660  cnvrcl0  43664  cnvtrcl0  43665  dfrtrcl5  43668  trrelsuperrel2dg  43710  dfrcl2  43713  relexp0a  43755  relexpaddss  43757  trclimalb2  43765  frege109d  43796  frege131d  43803  isotone1  44087  grumnudlem  44324  rnwf  45005  iblsplit  46010  fourierdlem46  46196  sge0resplit  46450  sge0split  46453  sge0splitmpt  46455  sge0xaddlem1  46477  sbgoldbo  47824  dfnbgrss  47889  gsumsplit2f  48217  setrec1  49729  elpglem2  49750