Theorem ssun2 4120

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 4119	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4099	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3971	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3888   ⊆ wss 3890

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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-un 3895  df-ss 3907

This theorem is referenced by:  ssun4  4122  elun2  4124  nsspssun  4209  unv  4340  un00  4386  pwunss  4560  snsspr2  4759  snsstp3  4762  fvrn0  6862  riotassuni  7357  ovima0  7539  unexb  7694  unexbOLD  7695  difex2  7707  rnexg  7846  xpord2indlem  8090  xpord3inddlem  8097  fnsuppres  8134  brtpos0  8176  frrlem14  8242  oaabs2  8578  domunsncan  9008  mapunen  9077  ac6sfi  9187  unfir  9211  domunfican  9225  iunfi  9246  elfiun  9336  dffi3  9337  hartogslem1  9450  unwdomg  9492  unxpwdom2  9496  unxpwdom  9497  trcl  9640  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  10556  canthp1lem2  10567  gchac  10595  wunrn  10643  wunex2  10652  inar1  10689  pnfxr  11190  ltrelxr  11197  un0mulcl  12462  fzdifsuc  13529  seqexw  13970  hashbclem  14405  hashf1lem1  14408  ccatrn  14543  trclublem  14948  relexprng  14999  fsumsplit  15694  o1fsum  15767  incexclem  15792  fprodsplit  15922  vdwlem5  16947  vdwlem8  16950  ramcl2  16978  srnginvl  17267  lmodvsca  17283  ipssca  17294  ipsvsca  17295  ipsip  17296  phlvsca  17304  phlip  17305  odrngtset  17361  odrngle  17362  odrngds  17363  prdssca  17410  prdsvsca  17414  prdsip  17415  prdsle  17416  prdsds  17418  prdstset  17420  prdshom  17421  prdsco  17422  imasds  17468  imassca  17474  imasvsca  17475  imasip  17476  imastset  17477  imasle  17478  mreexexlemd  17601  mreexexlem2d  17602  mreexexlem3d  17603  drsdirfi  18262  ipolerval  18489  psdmrn  18530  dirge  18560  grpinvfval  18945  mulgfval  19036  gsumzsplit  19893  gsumsplit2  19895  gsumzunsnd  19922  gsum2dlem2  19937  dprdfadd  19988  dmdprdsplit2lem  20013  dmdprdsplit2  20014  dmdprdsplit  20015  dprdsplit  20016  ablfac1eulem  20040  pgpfaclem1  20049  gsumle  20111  lspun  20973  lbsextlem2  21149  lbsextlem3  21150  lbsextlem4  21151  cnfldcj  21353  cnfldtset  21354  cnfldle  21355  cnfldds  21356  cnfldunif  21357  cnfldcjOLD  21366  cnfldtsetOLD  21367  cnfldleOLD  21368  cnflddsOLD  21369  cnfldunifOLD  21370  psrsca  21936  psrvscafval  21937  mplsubglem  21987  mplcoe5  22028  opsrtoslem2  22044  ordtbas2  23166  ordtbas  23167  ordtopn1  23169  ordtopn2  23170  leordtval2  23187  icomnfordt  23191  iooordt  23192  perfcls  23340  uncmp  23378  fiuncmp  23379  2ndcdisj2  23432  comppfsc  23507  1stckgenlem  23528  1stckgen  23529  ptbasin  23552  ptbasfi  23556  dfac14lem  23592  dfac14  23593  ptuncnv  23782  ptunhmeo  23783  ptcmpfi  23788  fbun  23815  filconn  23858  isufil2  23883  ufprim  23884  fin1aufil  23907  flimclslem  23959  flimfnfcls  24003  tmdgsum  24070  tsmsgsum  24114  tsmssplit  24127  tsmsxplem1  24128  trust  24204  prdsdsf  24342  prdsmet  24345  prdsbl  24466  cnmpopc  24905  rrxmetlem  25384  rrxmet  25385  rrxdstprj1  25386  ovolctb2  25469  ovolfiniun  25478  finiunmbl  25521  volfiniun  25524  uniioombllem3  25562  uniioombllem4  25563  mbfres2  25622  itg2splitlem  25725  itg2split  25726  itgsplit  25813  limcvallem  25848  ellimc2  25854  limccnp  25868  limccnp2  25869  limcco  25870  dvmptfsum  25952  lhop2  25992  lhop  25993  mdegcl  26044  elply2  26171  elplyd  26177  ply1term  26179  ply0  26183  plyaddlem1  26188  plymullem1  26189  plymullem  26191  mtest  26382  xrlimcnp  26945  jensen  26966  fsumharmonic  26989  chtdif  27135  lgsdir2lem3  27304  lgsquadlem2  27358  dchrisumlem2  27467  dchrisum0lem1b  27492  dchrisum0lem1  27493  pntrlog2bndlem6  27560  pntlemf  27582  nosupinfsep  27710  noetasuplem4  27714  noetalem1  27719  cofcutrtime  27933  addsuniflem  28007  addbday  28024  negsval  28031  mulsproplem12  28133  mulsproplem13  28134  mulsproplem14  28135  mulsuniflem  28155  mulsass  28172  precsexlem10  28222  bdayn0p1  28375  shsleji  31456  shsval2i  31473  ssjo  31533  sshhococi  31632  symgcom  33159  elrgspnsubrunlem1  33323  elrgspnsubrunlem2  33324  elrspunsn  33504  idlsrgtset  33583  vieta  33739  rtelextdg2  33887  constrextdg2lem  33908  esumsplit  34213  measun  34371  aean  34404  sxbrsigalem2  34446  bnj970  35105  bnj1137  35153  subfacp1lem2a  35378  subfacp1lem3  35380  subfacp1lem5  35382  erdszelem8  35396  kur14lem7  35410  cvmliftlem10  35492  mrsubvr  35709  refssfne  36556  topjoin  36563  tailf  36573  ttcuniun  36708  ttciunun  36709  bj-unrab  37249  bj-2upln1upl  37347  bj-ccinftyssccbar  37548  imadifss  37930  finixpnum  37940  matunitlindflem1  37951  mblfinlem4  37995  prdsbnd  38128  heibor1lem  38144  sspadd2  40276  pclfinN  40360  dochdmj1  41850  mzpcompact2lem  43197  eldioph2  43208  eldioph4b  43257  ttac  43482  pwssplit4  43535  isnumbasgrplem2  43550  isnumbasabl  43552  dfacbasgrp  43554  algsca  43623  algvsca  43624  fiuneneq  43638  tfsconcatrnss12  43795  rclexi  44060  rtrclex  44062  trclubgNEW  44063  trclexi  44065  rtrclexi  44066  cnvrcl0  44070  cnvtrcl0  44071  dfrtrcl5  44074  trrelsuperrel2dg  44116  dfrcl2  44119  relexp0a  44161  relexpaddss  44163  trclimalb2  44171  frege109d  44202  frege131d  44209  isotone1  44493  grumnudlem  44730  rnwf  45411  iblsplit  46412  fourierdlem46  46598  sge0resplit  46852  sge0split  46855  sge0splitmpt  46857  sge0xaddlem1  46879  sbgoldbo  48275  dfnbgrss  48340  gsumsplit2f  48668  setrec1  50178  elpglem2  50199