Theorem ssun2 4131

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 4130	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4110	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3982	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3899   ⊆ wss 3901

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 2115  ax-9 2123  ax-ext 2708

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 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-un 3906  df-ss 3918

This theorem is referenced by:  ssun4  4133  elun2  4135  nsspssun  4220  unv  4351  un00  4397  pwunss  4572  snsspr2  4771  snsstp3  4774  fvrn0  6862  riotassuni  7355  ovima0  7537  unexb  7692  unexbOLD  7693  difex2  7705  rnexg  7844  xpord2indlem  8089  xpord3inddlem  8096  fnsuppres  8133  brtpos0  8175  frrlem14  8241  oaabs2  8577  domunsncan  9005  mapunen  9074  ac6sfi  9184  unfir  9208  domunfican  9222  iunfi  9243  elfiun  9333  dffi3  9334  hartogslem1  9447  unwdomg  9489  unxpwdom2  9493  unxpwdom  9494  trcl  9637  unwf  9722  rankunb  9762  r0weon  9922  infxpenlem  9923  alephfplem4  10017  dju1dif  10083  cdainflem  10098  infdju  10117  cfsuc  10167  fin1a2lem10  10319  axdc3lem4  10363  ttukeylem7  10425  fpwwe2lem12  10553  canthp1lem2  10564  gchac  10592  wunrn  10640  wunex2  10649  inar1  10686  pnfxr  11186  ltrelxr  11193  un0mulcl  12435  fzdifsuc  13500  seqexw  13940  hashbclem  14375  hashf1lem1  14378  ccatrn  14513  trclublem  14918  relexprng  14969  fsumsplit  15664  o1fsum  15736  incexclem  15759  fprodsplit  15889  vdwlem5  16913  vdwlem8  16916  ramcl2  16944  srnginvl  17233  lmodvsca  17249  ipssca  17260  ipsvsca  17261  ipsip  17262  phlvsca  17270  phlip  17271  odrngtset  17327  odrngle  17328  odrngds  17329  prdssca  17376  prdsvsca  17380  prdsip  17381  prdsle  17382  prdsds  17384  prdstset  17386  prdshom  17387  prdsco  17388  imasds  17434  imassca  17440  imasvsca  17441  imasip  17442  imastset  17443  imasle  17444  mreexexlemd  17567  mreexexlem2d  17568  mreexexlem3d  17569  drsdirfi  18228  ipolerval  18455  psdmrn  18496  dirge  18526  grpinvfval  18908  mulgfval  18999  gsumzsplit  19856  gsumsplit2  19858  gsumzunsnd  19885  gsum2dlem2  19900  dprdfadd  19951  dmdprdsplit2lem  19976  dmdprdsplit2  19977  dmdprdsplit  19978  dprdsplit  19979  ablfac1eulem  20003  pgpfaclem1  20012  gsumle  20074  lspun  20938  lbsextlem2  21114  lbsextlem3  21115  lbsextlem4  21116  cnfldcj  21318  cnfldtset  21319  cnfldle  21320  cnfldds  21321  cnfldunif  21322  cnfldcjOLD  21331  cnfldtsetOLD  21332  cnfldleOLD  21333  cnflddsOLD  21334  cnfldunifOLD  21335  psrsca  21903  psrvscafval  21904  mplsubglem  21954  mplcoe5  21995  opsrtoslem2  22011  ordtbas2  23135  ordtbas  23136  ordtopn1  23138  ordtopn2  23139  leordtval2  23156  icomnfordt  23160  iooordt  23161  perfcls  23309  uncmp  23347  fiuncmp  23348  2ndcdisj2  23401  comppfsc  23476  1stckgenlem  23497  1stckgen  23498  ptbasin  23521  ptbasfi  23525  dfac14lem  23561  dfac14  23562  ptuncnv  23751  ptunhmeo  23752  ptcmpfi  23757  fbun  23784  filconn  23827  isufil2  23852  ufprim  23853  fin1aufil  23876  flimclslem  23928  flimfnfcls  23972  tmdgsum  24039  tsmsgsum  24083  tsmssplit  24096  tsmsxplem1  24097  trust  24173  prdsdsf  24311  prdsmet  24314  prdsbl  24435  cnmpopc  24878  rrxmetlem  25363  rrxmet  25364  rrxdstprj1  25365  ovolctb2  25449  ovolfiniun  25458  finiunmbl  25501  volfiniun  25504  uniioombllem3  25542  uniioombllem4  25543  mbfres2  25602  itg2splitlem  25705  itg2split  25706  itgsplit  25793  limcvallem  25828  ellimc2  25834  limccnp  25848  limccnp2  25849  limcco  25850  dvmptfsum  25935  lhop2  25976  lhop  25977  mdegcl  26030  elply2  26157  elplyd  26163  ply1term  26165  ply0  26169  plyaddlem1  26174  plymullem1  26175  plymullem  26177  mtest  26369  xrlimcnp  26934  jensen  26955  fsumharmonic  26978  chtdif  27124  lgsdir2lem3  27294  lgsquadlem2  27348  dchrisumlem2  27457  dchrisum0lem1b  27482  dchrisum0lem1  27483  pntrlog2bndlem6  27550  pntlemf  27572  nosupinfsep  27700  noetasuplem4  27704  noetalem1  27709  cofcutrtime  27923  addsuniflem  27997  addbday  28014  negsval  28021  mulsproplem12  28123  mulsproplem13  28124  mulsproplem14  28125  mulsuniflem  28145  mulsass  28162  precsexlem10  28212  bdayn0p1  28365  shsleji  31445  shsval2i  31462  ssjo  31522  sshhococi  31621  symgcom  33165  elrgspnsubrunlem1  33329  elrgspnsubrunlem2  33330  elrspunsn  33510  idlsrgtset  33589  vieta  33736  rtelextdg2  33884  constrextdg2lem  33905  esumsplit  34210  measun  34368  aean  34401  sxbrsigalem2  34443  bnj970  35103  bnj1137  35151  subfacp1lem2a  35374  subfacp1lem3  35376  subfacp1lem5  35378  erdszelem8  35392  kur14lem7  35406  cvmliftlem10  35488  mrsubvr  35705  refssfne  36552  topjoin  36559  tailf  36569  bj-unrab  37127  bj-2upln1upl  37225  bj-ccinftyssccbar  37423  imadifss  37796  finixpnum  37806  matunitlindflem1  37817  mblfinlem4  37861  prdsbnd  37994  heibor1lem  38010  sspadd2  40076  pclfinN  40160  dochdmj1  41650  mzpcompact2lem  42993  eldioph2  43004  eldioph4b  43053  ttac  43278  pwssplit4  43331  isnumbasgrplem2  43346  isnumbasabl  43348  dfacbasgrp  43350  algsca  43419  algvsca  43420  fiuneneq  43434  tfsconcatrnss12  43591  rclexi  43856  rtrclex  43858  trclubgNEW  43859  trclexi  43861  rtrclexi  43862  cnvrcl0  43866  cnvtrcl0  43867  dfrtrcl5  43870  trrelsuperrel2dg  43912  dfrcl2  43915  relexp0a  43957  relexpaddss  43959  trclimalb2  43967  frege109d  43998  frege131d  44005  isotone1  44289  grumnudlem  44526  rnwf  45207  iblsplit  46210  fourierdlem46  46396  sge0resplit  46650  sge0split  46653  sge0splitmpt  46655  sge0xaddlem1  46677  sbgoldbo  48033  dfnbgrss  48098  gsumsplit2f  48426  setrec1  49936  elpglem2  49957