Theorem ssun2 4132

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 4131	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4111	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3986	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3440  df-un 3910  df-ss 3922

This theorem is referenced by:  ssun4  4134  elun2  4136  nsspssun  4221  unv  4352  un00  4398  pwunss  4571  snsspr2  4769  snsstp3  4772  fvrn0  6854  riotassuni  7350  ovima0  7532  unexb  7687  unexbOLD  7688  difex2  7700  rnexg  7842  xpord2indlem  8087  xpord3inddlem  8094  fnsuppres  8131  brtpos0  8173  frrlem14  8239  oaabs2  8574  domunsncan  9001  mapunen  9070  ac6sfi  9189  unfir  9215  domunfican  9230  iunfi  9252  elfiun  9339  dffi3  9340  hartogslem1  9453  unwdomg  9495  unxpwdom2  9499  unxpwdom  9500  trcl  9643  unwf  9725  rankunb  9765  r0weon  9925  infxpenlem  9926  alephfplem4  10020  dju1dif  10086  cdainflem  10101  infdju  10120  cfsuc  10170  fin1a2lem10  10322  axdc3lem4  10366  ttukeylem7  10428  fpwwe2lem12  10555  canthp1lem2  10566  gchac  10594  wunrn  10642  wunex2  10651  inar1  10688  pnfxr  11188  ltrelxr  11195  un0mulcl  12436  fzdifsuc  13505  seqexw  13942  hashbclem  14377  hashf1lem1  14380  ccatrn  14514  trclublem  14920  relexprng  14971  fsumsplit  15666  o1fsum  15738  incexclem  15761  fprodsplit  15891  vdwlem5  16915  vdwlem8  16918  ramcl2  16946  srnginvl  17235  lmodvsca  17251  ipssca  17262  ipsvsca  17263  ipsip  17264  phlvsca  17272  phlip  17273  odrngtset  17329  odrngle  17330  odrngds  17331  prdssca  17378  prdsvsca  17382  prdsip  17383  prdsle  17384  prdsds  17386  prdstset  17388  prdshom  17389  prdsco  17390  imasds  17435  imassca  17441  imasvsca  17442  imasip  17443  imastset  17444  imasle  17445  mreexexlemd  17568  mreexexlem2d  17569  mreexexlem3d  17570  drsdirfi  18229  ipolerval  18456  psdmrn  18497  dirge  18527  grpinvfval  18875  mulgfval  18966  gsumzsplit  19824  gsumsplit2  19826  gsumzunsnd  19853  gsum2dlem2  19868  dprdfadd  19919  dmdprdsplit2lem  19944  dmdprdsplit2  19945  dmdprdsplit  19946  dprdsplit  19947  ablfac1eulem  19971  pgpfaclem1  19980  gsumle  20042  lspun  20908  lbsextlem2  21084  lbsextlem3  21085  lbsextlem4  21086  cnfldcj  21288  cnfldtset  21289  cnfldle  21290  cnfldds  21291  cnfldunif  21292  cnfldcjOLD  21301  cnfldtsetOLD  21302  cnfldleOLD  21303  cnflddsOLD  21304  cnfldunifOLD  21305  psrsca  21872  psrvscafval  21873  mplsubglem  21924  mplcoe5  21963  opsrtoslem2  21979  ordtbas2  23094  ordtbas  23095  ordtopn1  23097  ordtopn2  23098  leordtval2  23115  icomnfordt  23119  iooordt  23120  perfcls  23268  uncmp  23306  fiuncmp  23307  2ndcdisj2  23360  comppfsc  23435  1stckgenlem  23456  1stckgen  23457  ptbasin  23480  ptbasfi  23484  dfac14lem  23520  dfac14  23521  ptuncnv  23710  ptunhmeo  23711  ptcmpfi  23716  fbun  23743  filconn  23786  isufil2  23811  ufprim  23812  fin1aufil  23835  flimclslem  23887  flimfnfcls  23931  tmdgsum  23998  tsmsgsum  24042  tsmssplit  24055  tsmsxplem1  24056  trust  24133  prdsdsf  24271  prdsmet  24274  prdsbl  24395  cnmpopc  24838  rrxmetlem  25323  rrxmet  25324  rrxdstprj1  25325  ovolctb2  25409  ovolfiniun  25418  finiunmbl  25461  volfiniun  25464  uniioombllem3  25502  uniioombllem4  25503  mbfres2  25562  itg2splitlem  25665  itg2split  25666  itgsplit  25753  limcvallem  25788  ellimc2  25794  limccnp  25808  limccnp2  25809  limcco  25810  dvmptfsum  25895  lhop2  25936  lhop  25937  mdegcl  25990  elply2  26117  elplyd  26123  ply1term  26125  ply0  26129  plyaddlem1  26134  plymullem1  26135  plymullem  26137  mtest  26329  xrlimcnp  26894  jensen  26915  fsumharmonic  26938  chtdif  27084  lgsdir2lem3  27254  lgsquadlem2  27308  dchrisumlem2  27417  dchrisum0lem1b  27442  dchrisum0lem1  27443  pntrlog2bndlem6  27510  pntlemf  27532  nosupinfsep  27660  noetasuplem4  27664  noetalem1  27669  cofcutrtime  27858  addsuniflem  27931  addsbday  27947  negsval  27954  mulsproplem12  28053  mulsproplem13  28054  mulsproplem14  28055  mulsuniflem  28075  mulsass  28092  precsexlem10  28141  bdayn0p1  28281  shsleji  31332  shsval2i  31349  ssjo  31409  sshhococi  31508  symgcom  33038  elrgspnsubrunlem1  33200  elrgspnsubrunlem2  33201  elrspunsn  33379  idlsrgtset  33458  rtelextdg2  33696  constrextdg2lem  33717  esumsplit  34022  measun  34180  aean  34213  sxbrsigalem2  34256  bnj970  34916  bnj1137  34964  subfacp1lem2a  35155  subfacp1lem3  35157  subfacp1lem5  35159  erdszelem8  35173  kur14lem7  35187  cvmliftlem10  35269  mrsubvr  35486  refssfne  36334  topjoin  36341  tailf  36351  bj-unrab  36902  bj-2upln1upl  37000  bj-ccinftyssccbar  37194  imadifss  37577  finixpnum  37587  matunitlindflem1  37598  mblfinlem4  37642  prdsbnd  37775  heibor1lem  37791  sspadd2  39798  pclfinN  39882  dochdmj1  41372  mzpcompact2lem  42727  eldioph2  42738  eldioph4b  42787  ttac  43012  pwssplit4  43065  isnumbasgrplem2  43080  isnumbasabl  43082  dfacbasgrp  43084  algsca  43153  algvsca  43154  fiuneneq  43168  tfsconcatrnss12  43325  rclexi  43591  rtrclex  43593  trclubgNEW  43594  trclexi  43596  rtrclexi  43597  cnvrcl0  43601  cnvtrcl0  43602  dfrtrcl5  43605  trrelsuperrel2dg  43647  dfrcl2  43650  relexp0a  43692  relexpaddss  43694  trclimalb2  43702  frege109d  43733  frege131d  43740  isotone1  44024  grumnudlem  44261  rnwf  44943  iblsplit  45951  fourierdlem46  46137  sge0resplit  46391  sge0split  46394  sge0splitmpt  46396  sge0xaddlem1  46418  sbgoldbo  47775  dfnbgrss  47840  gsumsplit2f  48168  setrec1  49680  elpglem2  49701