Theorem ssun2 4119

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 4118	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4098	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3970	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3887   ⊆ wss 3889

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 2708

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

This theorem is referenced by:  ssun4  4121  elun2  4123  nsspssun  4208  unv  4339  un00  4385  pwunss  4559  snsspr2  4758  snsstp3  4761  fvrn0  6868  riotassuni  7364  ovima0  7546  unexb  7701  unexbOLD  7702  difex2  7714  rnexg  7853  xpord2indlem  8097  xpord3inddlem  8104  fnsuppres  8141  brtpos0  8183  frrlem14  8249  oaabs2  8585  domunsncan  9015  mapunen  9084  ac6sfi  9194  unfir  9218  domunfican  9232  iunfi  9253  elfiun  9343  dffi3  9344  hartogslem1  9457  unwdomg  9499  unxpwdom2  9503  unxpwdom  9504  trcl  9649  unwf  9734  rankunb  9774  r0weon  9934  infxpenlem  9935  alephfplem4  10029  dju1dif  10095  cdainflem  10110  infdju  10129  cfsuc  10179  fin1a2lem10  10331  axdc3lem4  10375  ttukeylem7  10437  fpwwe2lem12  10565  canthp1lem2  10576  gchac  10604  wunrn  10652  wunex2  10661  inar1  10698  pnfxr  11199  ltrelxr  11206  un0mulcl  12471  fzdifsuc  13538  seqexw  13979  hashbclem  14414  hashf1lem1  14417  ccatrn  14552  trclublem  14957  relexprng  15008  fsumsplit  15703  o1fsum  15776  incexclem  15801  fprodsplit  15931  vdwlem5  16956  vdwlem8  16959  ramcl2  16987  srnginvl  17276  lmodvsca  17292  ipssca  17303  ipsvsca  17304  ipsip  17305  phlvsca  17313  phlip  17314  odrngtset  17370  odrngle  17371  odrngds  17372  prdssca  17419  prdsvsca  17423  prdsip  17424  prdsle  17425  prdsds  17427  prdstset  17429  prdshom  17430  prdsco  17431  imasds  17477  imassca  17483  imasvsca  17484  imasip  17485  imastset  17486  imasle  17487  mreexexlemd  17610  mreexexlem2d  17611  mreexexlem3d  17612  drsdirfi  18271  ipolerval  18498  psdmrn  18539  dirge  18569  grpinvfval  18954  mulgfval  19045  gsumzsplit  19902  gsumsplit2  19904  gsumzunsnd  19931  gsum2dlem2  19946  dprdfadd  19997  dmdprdsplit2lem  20022  dmdprdsplit2  20023  dmdprdsplit  20024  dprdsplit  20025  ablfac1eulem  20049  pgpfaclem1  20058  gsumle  20120  lspun  20982  lbsextlem2  21157  lbsextlem3  21158  lbsextlem4  21159  cnfldcj  21361  cnfldtset  21362  cnfldle  21363  cnfldds  21364  cnfldunif  21365  psrsca  21926  psrvscafval  21927  mplsubglem  21977  mplcoe5  22018  opsrtoslem2  22034  ordtbas2  23156  ordtbas  23157  ordtopn1  23159  ordtopn2  23160  leordtval2  23177  icomnfordt  23181  iooordt  23182  perfcls  23330  uncmp  23368  fiuncmp  23369  2ndcdisj2  23422  comppfsc  23497  1stckgenlem  23518  1stckgen  23519  ptbasin  23542  ptbasfi  23546  dfac14lem  23582  dfac14  23583  ptuncnv  23772  ptunhmeo  23773  ptcmpfi  23778  fbun  23805  filconn  23848  isufil2  23873  ufprim  23874  fin1aufil  23897  flimclslem  23949  flimfnfcls  23993  tmdgsum  24060  tsmsgsum  24104  tsmssplit  24117  tsmsxplem1  24118  trust  24194  prdsdsf  24332  prdsmet  24335  prdsbl  24456  cnmpopc  24895  rrxmetlem  25374  rrxmet  25375  rrxdstprj1  25376  ovolctb2  25459  ovolfiniun  25468  finiunmbl  25511  volfiniun  25514  uniioombllem3  25552  uniioombllem4  25553  mbfres2  25612  itg2splitlem  25715  itg2split  25716  itgsplit  25803  limcvallem  25838  ellimc2  25844  limccnp  25858  limccnp2  25859  limcco  25860  dvmptfsum  25942  lhop2  25982  lhop  25983  mdegcl  26034  elply2  26161  elplyd  26167  ply1term  26169  ply0  26173  plyaddlem1  26178  plymullem1  26179  plymullem  26181  mtest  26369  xrlimcnp  26932  jensen  26952  fsumharmonic  26975  chtdif  27121  lgsdir2lem3  27290  lgsquadlem2  27344  dchrisumlem2  27453  dchrisum0lem1b  27478  dchrisum0lem1  27479  pntrlog2bndlem6  27546  pntlemf  27568  nosupinfsep  27696  noetasuplem4  27700  noetalem1  27705  cofcutrtime  27919  addsuniflem  27993  addbday  28010  negsval  28017  mulsproplem12  28119  mulsproplem13  28120  mulsproplem14  28121  mulsuniflem  28141  mulsass  28158  precsexlem10  28208  bdayn0p1  28361  shsleji  31441  shsval2i  31458  ssjo  31518  sshhococi  31617  symgcom  33144  elrgspnsubrunlem1  33308  elrgspnsubrunlem2  33309  elrspunsn  33489  idlsrgtset  33568  vieta  33724  rtelextdg2  33871  constrextdg2lem  33892  esumsplit  34197  measun  34355  aean  34388  sxbrsigalem2  34430  bnj970  35089  bnj1137  35137  subfacp1lem2a  35362  subfacp1lem3  35364  subfacp1lem5  35366  erdszelem8  35380  kur14lem7  35394  cvmliftlem10  35476  mrsubvr  35693  refssfne  36540  topjoin  36547  tailf  36557  ttcuniun  36692  ttciunun  36693  bj-unrab  37233  bj-2upln1upl  37331  bj-ccinftyssccbar  37532  imadifss  37916  finixpnum  37926  matunitlindflem1  37937  mblfinlem4  37981  prdsbnd  38114  heibor1lem  38130  sspadd2  40262  pclfinN  40346  dochdmj1  41836  mzpcompact2lem  43183  eldioph2  43194  eldioph4b  43239  ttac  43464  pwssplit4  43517  isnumbasgrplem2  43532  isnumbasabl  43534  dfacbasgrp  43536  algsca  43605  algvsca  43606  fiuneneq  43620  tfsconcatrnss12  43777  rclexi  44042  rtrclex  44044  trclubgNEW  44045  trclexi  44047  rtrclexi  44048  cnvrcl0  44052  cnvtrcl0  44053  dfrtrcl5  44056  trrelsuperrel2dg  44098  dfrcl2  44101  relexp0a  44143  relexpaddss  44145  trclimalb2  44153  frege109d  44184  frege131d  44191  isotone1  44475  grumnudlem  44712  rnwf  45393  iblsplit  46394  fourierdlem46  46580  sge0resplit  46834  sge0split  46837  sge0splitmpt  46839  sge0xaddlem1  46861  sbgoldbo  48263  dfnbgrss  48328  gsumsplit2f  48656  setrec1  50166  elpglem2  50187