Theorem ssun2 4173

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 4172	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4153	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4018	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3946   ⊆ wss 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-un 3953  df-in 3955  df-ss 3965

This theorem is referenced by:  ssun4  4175  elun2  4177  nsspssun  4257  unv  4395  un00  4442  pwunss  4620  snsspr2  4818  snsstp3  4821  fvrn0  6921  riotassuni  7405  ovima0  7585  unexb  7734  difex2  7746  rnexg  7894  xpord2indlem  8132  xpord3inddlem  8139  fnsuppres  8175  brtpos0  8217  frrlem14  8283  wfrlem16OLD  8323  oaabs2  8647  domunsncan  9071  mapunen  9145  ac6sfi  9286  unfir  9313  domunfican  9319  iunfi  9339  elfiun  9424  dffi3  9425  hartogslem1  9536  unwdomg  9578  unxpwdom2  9582  unxpwdom  9583  trcl  9722  unwf  9804  rankunb  9844  r0weon  10006  infxpenlem  10007  alephfplem4  10101  dju1dif  10166  cdainflem  10181  infdju  10202  cfsuc  10251  fin1a2lem10  10403  axdc3lem4  10447  ttukeylem7  10509  fpwwe2lem12  10636  canthp1lem2  10647  gchac  10675  wunrn  10723  wunex2  10732  inar1  10769  pnfxr  11267  ltrelxr  11274  un0mulcl  12505  fzdifsuc  13560  seqexw  13981  hashbclem  14410  hashf1lem1  14414  hashf1lem1OLD  14415  ccatrn  14538  trclublem  14941  relexprng  14992  fsumsplit  15686  o1fsum  15758  incexclem  15781  fprodsplit  15909  vdwlem5  16917  vdwlem8  16920  ramcl2  16948  srnginvl  17257  lmodvsca  17273  ipssca  17284  ipsvsca  17285  ipsip  17286  phlvsca  17294  phlip  17295  odrngtset  17351  odrngle  17352  odrngds  17353  prdssca  17401  prdsvsca  17405  prdsip  17406  prdsle  17407  prdsds  17409  prdstset  17411  prdshom  17412  prdsco  17413  imasds  17458  imassca  17464  imasvsca  17465  imasip  17466  imastset  17467  imasle  17468  mreexexlemd  17587  mreexexlem2d  17588  mreexexlem3d  17589  drsdirfi  18257  ipolerval  18484  psdmrn  18525  dirge  18555  grpinvfval  18862  mulgfval  18951  gsumzsplit  19794  gsumsplit2  19796  gsumzunsnd  19823  gsum2dlem2  19838  dprdfadd  19889  dmdprdsplit2lem  19914  dmdprdsplit2  19915  dmdprdsplit  19916  dprdsplit  19917  ablfac1eulem  19941  pgpfaclem1  19950  lspun  20597  lbsextlem2  20771  lbsextlem3  20772  lbsextlem4  20773  cnfldcj  20950  cnfldtset  20951  cnfldle  20952  cnfldds  20953  cnfldunif  20954  psrbagaddclOLD  21481  psrsca  21507  psrvscafval  21508  mplsubglem  21557  mplcoe5  21594  opsrtoslem2  21616  ordtbas2  22694  ordtbas  22695  ordtopn1  22697  ordtopn2  22698  leordtval2  22715  icomnfordt  22719  iooordt  22720  perfcls  22868  uncmp  22906  fiuncmp  22907  2ndcdisj2  22960  comppfsc  23035  1stckgenlem  23056  1stckgen  23057  ptbasin  23080  ptbasfi  23084  dfac14lem  23120  dfac14  23121  ptuncnv  23310  ptunhmeo  23311  ptcmpfi  23316  fbun  23343  filconn  23386  isufil2  23411  ufprim  23412  fin1aufil  23435  flimclslem  23487  flimfnfcls  23531  tmdgsum  23598  tsmsgsum  23642  tsmssplit  23655  tsmsxplem1  23656  trust  23733  prdsdsf  23872  prdsmet  23875  prdsbl  23999  cnmpopc  24443  rrxmetlem  24923  rrxmet  24924  rrxdstprj1  24925  ovolctb2  25008  ovolfiniun  25017  finiunmbl  25060  volfiniun  25063  uniioombllem3  25101  uniioombllem4  25102  mbfres2  25161  itg2splitlem  25265  itg2split  25266  itgsplit  25352  limcvallem  25387  ellimc2  25393  limccnp  25407  limccnp2  25408  limcco  25409  dvmptfsum  25491  lhop2  25531  lhop  25532  mdegcl  25586  elply2  25709  elplyd  25715  ply1term  25717  ply0  25721  plyaddlem1  25726  plymullem1  25727  plymullem  25729  mtest  25915  xrlimcnp  26470  jensen  26490  fsumharmonic  26513  chtdif  26659  lgsdir2lem3  26827  lgsquadlem2  26881  dchrisumlem2  26990  dchrisum0lem1b  27015  dchrisum0lem1  27016  pntrlog2bndlem6  27083  pntlemf  27105  nosupinfsep  27232  noetasuplem4  27236  noetalem1  27241  cofcutrtime  27411  addsuniflem  27481  negsval  27497  mulsproplem12  27580  mulsproplem13  27581  mulsproplem14  27582  mulsuniflem  27601  mulsass  27618  precsexlem10  27659  shsleji  30618  shsval2i  30635  ssjo  30695  sshhococi  30794  gsumle  32237  symgcom  32239  elrspunsn  32542  idlsrgtset  32617  esumsplit  33046  measun  33204  aean  33237  sxbrsigalem2  33280  bnj970  33953  bnj1137  34001  subfacp1lem2a  34166  subfacp1lem3  34168  subfacp1lem5  34170  erdszelem8  34184  kur14lem7  34198  cvmliftlem10  34280  mrsubvr  34497  refssfne  35238  topjoin  35245  tailf  35255  bj-unrab  35801  bj-2upln1upl  35900  bj-ccinftyssccbar  36094  imadifss  36458  finixpnum  36468  matunitlindflem1  36479  mblfinlem4  36523  prdsbnd  36656  heibor1lem  36672  sspadd2  38682  pclfinN  38766  dochdmj1  40256  mzpcompact2lem  41479  eldioph2  41490  eldioph4b  41539  ttac  41765  pwssplit4  41821  isnumbasgrplem2  41836  isnumbasabl  41838  dfacbasgrp  41840  algsca  41913  algvsca  41914  fiuneneq  41929  tfsconcatrnss12  42089  rclexi  42356  rtrclex  42358  trclubgNEW  42359  trclexi  42361  rtrclexi  42362  cnvrcl0  42366  cnvtrcl0  42367  dfrtrcl5  42370  trrelsuperrel2dg  42412  dfrcl2  42415  relexp0a  42457  relexpaddss  42459  trclimalb2  42467  frege109d  42498  frege131d  42505  isotone1  42789  grumnudlem  43034  iblsplit  44672  fourierdlem46  44858  sge0resplit  45112  sge0split  45115  sge0splitmpt  45117  sge0xaddlem1  45139  sbgoldbo  46445  gsumsplit2f  46580  setrec1  47726  elpglem2  47747