Theorem ssun2 4140

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 4139	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4120	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3993	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3911   ⊆ wss 3913

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-un 3918  df-ss 3930

This theorem is referenced by:  ssun4  4142  elun2  4144  nsspssun  4229  unv  4362  un00  4408  pwunss  4582  snsspr2  4782  snsstp3  4785  fvrn0  6907  riotassuni  7405  ovima0  7587  unexb  7742  unexbOLD  7743  difex2  7755  rnexg  7895  xpord2indlem  8139  xpord3inddlem  8146  fnsuppres  8183  brtpos0  8225  frrlem14  8292  oaabs2  8631  domunsncan  9061  mapunen  9130  ac6sfi  9240  unfir  9264  domunfican  9277  iunfi  9296  elfiun  9386  dffi3  9387  hartogslem1  9500  unwdomg  9542  unxpwdom2  9546  unxpwdom  9547  trcl  9693  unwf  9778  rankunb  9818  r0weon  9992  infxpenlem  9993  alephfplem4  10087  dju1dif  10152  cdainflem  10167  infdju  10186  cfsuc  10237  fin1a2lem10  10389  axdc3lem4  10433  ttukeylem7  10495  fpwwe2lem12  10623  canthp1lem2  10634  gchac  10662  wunrn  10710  wunex2  10719  inar1  10756  pnfxr  11259  ltrelxr  11266  un0mulcl  12534  fzdifsuc  13608  seqexw  14049  hashbclem  14485  hashf1lem1  14488  ccatrn  14623  trclublem  15028  relexprng  15079  fsumsplit  15788  o1fsum  15861  incexclem  15886  fprodsplit  16016  vdwlem5  17041  vdwlem8  17044  ramcl2  17072  srnginvl  17362  lmodvsca  17378  ipssca  17389  ipsvsca  17390  ipsip  17391  phlvsca  17399  phlip  17400  odrngtset  17456  odrngle  17457  odrngds  17458  prdssca  17505  prdsvsca  17509  prdsip  17510  prdsle  17511  prdsds  17513  prdstset  17515  prdshom  17516  prdsco  17517  imasds  17563  imassca  17569  imasvsca  17570  imasip  17571  imastset  17572  imasle  17573  mreexexlemd  17696  mreexexlem2d  17697  mreexexlem3d  17698  drsdirfi  18357  ipolerval  18584  psdmrn  18625  dirge  18655  grpinvfval  19041  mulgfval  19131  gsumzsplit  19993  gsumsplit2  19995  gsumzunsnd  20022  gsum2dlem2  20037  dprdfadd  20088  dmdprdsplit2lem  20113  dmdprdsplit2  20114  dmdprdsplit  20115  dprdsplit  20116  ablfac1eulem  20140  pgpfaclem1  20149  gsumle  20211  lspun  21082  lbsextlem2  21257  lbsextlem3  21258  lbsextlem4  21259  cnfldcj  21496  cnfldtset  21497  cnfldle  21498  cnfldds  21499  cnfldunif  21500  psrsca  22062  psrvscafval  22063  mplsubglem  22113  mplcoe5  22156  opsrtoslem2  22172  ordtbas2  23313  ordtbas  23314  ordtopn1  23316  ordtopn2  23317  leordtval2  23334  icomnfordt  23338  iooordt  23339  perfcls  23487  uncmp  23525  fiuncmp  23526  2ndcdisj2  23579  comppfsc  23654  1stckgenlem  23675  1stckgen  23676  ptbasin  23699  ptbasfi  23703  dfac14lem  23739  dfac14  23740  ptuncnv  23929  ptunhmeo  23930  ptcmpfi  23935  fbun  23962  filconn  24005  isufil2  24030  ufprim  24031  fin1aufil  24054  flimclslem  24106  flimfnfcls  24150  tmdgsum  24217  tsmsgsum  24261  tsmssplit  24274  tsmsxplem1  24275  trust  24351  prdsdsf  24489  prdsmet  24492  prdsbl  24613  cnmpopc  25052  rrxmetlem  25531  rrxmet  25532  rrxdstprj1  25533  ovolctb2  25616  ovolfiniun  25625  finiunmbl  25668  volfiniun  25671  uniioombllem3  25709  uniioombllem4  25710  mbfres2  25769  itg2splitlem  25872  itg2split  25873  itgsplit  25960  limcvallem  25995  ellimc2  26001  limccnp  26015  limccnp2  26016  limcco  26017  dvmptfsum  26099  lhop2  26139  lhop  26140  mdegcl  26191  elply2  26318  elplyd  26324  ply1term  26326  ply0  26330  plyaddlem1  26335  plymullem1  26336  plymullem  26338  mtest  26529  xrlimcnp  27095  jensen  27115  fsumharmonic  27138  chtdif  27284  lgsdir2lem3  27453  lgsquadlem2  27507  dchrisumlem2  27616  dchrisum0lem1b  27641  dchrisum0lem1  27642  pntrlog2bndlem6  27709  pntlemf  27731  nosupinfsep  27858  noetasuplem4  27862  noetalem1  27867  cofcutrtime  28082  addsuniflem  28156  addbday  28173  negsval  28180  mulsproplem12  28282  mulsproplem13  28283  mulsproplem14  28284  mulsuniflem  28304  mulsass  28321  precsexlem10  28371  bdayn0p1  28524  shsleji  31659  shsval2i  31676  ssjo  31736  sshhococi  31835  symgcom  33340  elrgspnsubrunlem1  33504  elrgspnsubrunlem2  33505  elrspunsn  33677  idlsrgtset  33739  vieta  33911  rtelextdg2  34058  constrextdg2lem  34079  esumsplit  34384  measun  34542  aean  34575  sxbrsigalem2  34617  bnj970  35276  bnj1137  35324  subfacp1lem2a  35567  subfacp1lem3  35569  subfacp1lem5  35571  erdszelem8  35585  kur14lem7  35599  cvmliftlem10  35681  mrsubvr  35898  refssfne  36754  topjoin  36761  tailf  36771  ttcuniun  36906  ttciunun  36907  bj-unrab  37446  bj-2upln1upl  37544  bj-ccinftyssccbar  37745  imadifss  38129  finixpnum  38139  matunitlindflem1  38150  mblfinlem4  38194  prdsbnd  38327  heibor1lem  38343  sspadd2  40475  pclfinN  40559  dochdmj1  42049  mzpcompact2lem  43367  eldioph2  43378  eldioph4b  43423  ttac  43648  pwssplit4  43701  isnumbasgrplem2  43716  isnumbasabl  43718  dfacbasgrp  43720  algsca  43789  algvsca  43790  fiuneneq  43804  tfsconcatrnss12  43961  rclexi  44226  rtrclex  44228  trclubgNEW  44229  trclexi  44231  rtrclexi  44232  cnvrcl0  44236  cnvtrcl0  44237  dfrtrcl5  44240  trrelsuperrel2dg  44282  dfrcl2  44285  relexp0a  44327  relexpaddss  44329  trclimalb2  44337  frege109d  44368  frege131d  44375  isotone1  44659  grumnudlem  44880  rnwf  45560  iblsplit  46565  fourierdlem46  46751  sge0resplit  47005  sge0split  47008  sge0splitmpt  47010  sge0xaddlem1  47032  sbgoldbo  48434  dfnbgrss  48499  gsumsplit2f  48827  setrec1  50347  elpglem2  50368