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 4109	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3982	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 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3907  df-ss 3919

This theorem is referenced by:  ssun4  4131  elun2  4133  nsspssun  4218  unv  4350  un00  4396  pwunss  4570  snsspr2  4770  snsstp3  4773  fvrn0  6890  riotassuni  7388  ovima0  7570  unexb  7725  unexbOLD  7726  difex2  7738  rnexg  7878  xpord2indlem  8121  xpord3inddlem  8128  fnsuppres  8165  brtpos0  8207  frrlem14  8274  oaabs2  8613  domunsncan  9043  mapunen  9112  ac6sfi  9222  unfir  9246  domunfican  9260  iunfi  9280  elfiun  9370  dffi3  9371  hartogslem1  9484  unwdomg  9526  unxpwdom2  9530  unxpwdom  9531  trcl  9677  unwf  9762  rankunb  9802  r0weon  9962  infxpenlem  9963  alephfplem4  10057  dju1dif  10123  cdainflem  10138  infdju  10157  cfsuc  10208  fin1a2lem10  10360  axdc3lem4  10404  ttukeylem7  10466  fpwwe2lem12  10594  canthp1lem2  10605  gchac  10633  wunrn  10681  wunex2  10690  inar1  10727  pnfxr  11230  ltrelxr  11237  un0mulcl  12509  fzdifsuc  13583  seqexw  14024  hashbclem  14459  hashf1lem1  14462  ccatrn  14597  trclublem  15002  relexprng  15053  fsumsplit  15759  o1fsum  15832  incexclem  15857  fprodsplit  15987  vdwlem5  17012  vdwlem8  17015  ramcl2  17043  srnginvl  17333  lmodvsca  17349  ipssca  17360  ipsvsca  17361  ipsip  17362  phlvsca  17370  phlip  17371  odrngtset  17427  odrngle  17428  odrngds  17429  prdssca  17476  prdsvsca  17480  prdsip  17481  prdsle  17482  prdsds  17484  prdstset  17486  prdshom  17487  prdsco  17488  imasds  17534  imassca  17540  imasvsca  17541  imasip  17542  imastset  17543  imasle  17544  mreexexlemd  17667  mreexexlem2d  17668  mreexexlem3d  17669  drsdirfi  18328  ipolerval  18555  psdmrn  18596  dirge  18626  grpinvfval  19011  mulgfval  19102  gsumzsplit  19958  gsumsplit2  19960  gsumzunsnd  19987  gsum2dlem2  20002  dprdfadd  20053  dmdprdsplit2lem  20078  dmdprdsplit2  20079  dmdprdsplit  20080  dprdsplit  20081  ablfac1eulem  20105  pgpfaclem1  20114  gsumle  20176  lspun  21042  lbsextlem2  21217  lbsextlem3  21218  lbsextlem4  21219  cnfldcj  21421  cnfldtset  21422  cnfldle  21423  cnfldds  21424  cnfldunif  21425  psrsca  21987  psrvscafval  21988  mplsubglem  22038  mplcoe5  22081  opsrtoslem2  22097  ordtbas2  23239  ordtbas  23240  ordtopn1  23242  ordtopn2  23243  leordtval2  23260  icomnfordt  23264  iooordt  23265  perfcls  23413  uncmp  23451  fiuncmp  23452  2ndcdisj2  23505  comppfsc  23580  1stckgenlem  23601  1stckgen  23602  ptbasin  23625  ptbasfi  23629  dfac14lem  23665  dfac14  23666  ptuncnv  23855  ptunhmeo  23856  ptcmpfi  23861  fbun  23888  filconn  23931  isufil2  23956  ufprim  23957  fin1aufil  23980  flimclslem  24032  flimfnfcls  24076  tmdgsum  24143  tsmsgsum  24187  tsmssplit  24200  tsmsxplem1  24201  trust  24277  prdsdsf  24415  prdsmet  24418  prdsbl  24539  cnmpopc  24978  rrxmetlem  25457  rrxmet  25458  rrxdstprj1  25459  ovolctb2  25542  ovolfiniun  25551  finiunmbl  25594  volfiniun  25597  uniioombllem3  25635  uniioombllem4  25636  mbfres2  25695  itg2splitlem  25798  itg2split  25799  itgsplit  25886  limcvallem  25921  ellimc2  25927  limccnp  25941  limccnp2  25942  limcco  25943  dvmptfsum  26025  lhop2  26065  lhop  26066  mdegcl  26117  elply2  26244  elplyd  26250  ply1term  26252  ply0  26256  plyaddlem1  26261  plymullem1  26262  plymullem  26264  mtest  26455  xrlimcnp  27021  jensen  27041  fsumharmonic  27064  chtdif  27210  lgsdir2lem3  27379  lgsquadlem2  27433  dchrisumlem2  27542  dchrisum0lem1b  27567  dchrisum0lem1  27568  pntrlog2bndlem6  27635  pntlemf  27657  nosupinfsep  27784  noetasuplem4  27788  noetalem1  27793  cofcutrtime  28008  addsuniflem  28082  addbday  28099  negsval  28106  mulsproplem12  28208  mulsproplem13  28209  mulsproplem14  28210  mulsuniflem  28230  mulsass  28247  precsexlem10  28297  bdayn0p1  28450  shsleji  31530  shsval2i  31547  ssjo  31607  sshhococi  31706  symgcom  33224  elrgspnsubrunlem1  33389  elrgspnsubrunlem2  33390  elrspunsn  33576  idlsrgtset  33665  vieta  33838  rtelextdg2  33985  constrextdg2lem  34006  esumsplit  34311  measun  34469  aean  34502  sxbrsigalem2  34544  bnj970  35203  bnj1137  35251  subfacp1lem2a  35491  subfacp1lem3  35493  subfacp1lem5  35495  erdszelem8  35509  kur14lem7  35523  cvmliftlem10  35605  mrsubvr  35822  refssfne  36679  topjoin  36686  tailf  36696  ttcuniun  36831  ttciunun  36832  bj-unrab  37372  bj-2upln1upl  37470  bj-ccinftyssccbar  37671  imadifss  38055  finixpnum  38065  matunitlindflem1  38076  mblfinlem4  38120  prdsbnd  38253  heibor1lem  38269  sspadd2  40401  pclfinN  40485  dochdmj1  41975  mzpcompact2lem  43293  eldioph2  43304  eldioph4b  43349  ttac  43574  pwssplit4  43627  isnumbasgrplem2  43642  isnumbasabl  43644  dfacbasgrp  43646  algsca  43715  algvsca  43716  fiuneneq  43730  tfsconcatrnss12  43887  rclexi  44152  rtrclex  44154  trclubgNEW  44155  trclexi  44157  rtrclexi  44158  cnvrcl0  44162  cnvtrcl0  44163  dfrtrcl5  44166  trrelsuperrel2dg  44208  dfrcl2  44211  relexp0a  44253  relexpaddss  44255  trclimalb2  44263  frege109d  44294  frege131d  44301  isotone1  44585  grumnudlem  44822  rnwf  45503  iblsplit  46501  fourierdlem46  46687  sge0resplit  46941  sge0split  46944  sge0splitmpt  46946  sge0xaddlem1  46968  sbgoldbo  48370  dfnbgrss  48435  gsumsplit2f  48763  setrec1  50273  elpglem2  50294