Theorem ssun2 4108

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 4107	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4088	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3963	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3881   ⊆ wss 3883

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 854  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-un 3888  df-ss 3900

This theorem is referenced by:  ssun4  4110  elun2  4112  nsspssun  4196  unv  4327  un00  4373  pwunss  4547  snsspr2  4746  snsstp3  4749  fvrn0  6855  riotassuni  7353  ovima0  7535  unexb  7690  unexbOLD  7691  difex2  7703  rnexg  7842  xpord2indlem  8087  xpord3inddlem  8094  fnsuppres  8131  brtpos0  8173  frrlem14  8239  oaabs2  8575  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  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  20977  lbsextlem2  21152  lbsextlem3  21153  lbsextlem4  21154  cnfldcj  21356  cnfldtset  21357  cnfldle  21358  cnfldds  21359  cnfldunif  21360  psrsca  21922  psrvscafval  21923  mplsubglem  21973  mplcoe5  22016  opsrtoslem2  22032  ordtbas2  23174  ordtbas  23175  ordtopn1  23177  ordtopn2  23178  leordtval2  23195  icomnfordt  23199  iooordt  23200  perfcls  23348  uncmp  23386  fiuncmp  23387  2ndcdisj2  23440  comppfsc  23515  1stckgenlem  23536  1stckgen  23537  ptbasin  23560  ptbasfi  23564  dfac14lem  23600  dfac14  23601  ptuncnv  23790  ptunhmeo  23791  ptcmpfi  23796  fbun  23823  filconn  23866  isufil2  23891  ufprim  23892  fin1aufil  23915  flimclslem  23967  flimfnfcls  24011  tmdgsum  24078  tsmsgsum  24122  tsmssplit  24135  tsmsxplem1  24136  trust  24212  prdsdsf  24350  prdsmet  24353  prdsbl  24474  cnmpopc  24913  rrxmetlem  25392  rrxmet  25393  rrxdstprj1  25394  ovolctb2  25477  ovolfiniun  25486  finiunmbl  25529  volfiniun  25532  uniioombllem3  25570  uniioombllem4  25571  mbfres2  25630  itg2splitlem  25733  itg2split  25734  itgsplit  25821  limcvallem  25856  ellimc2  25862  limccnp  25876  limccnp2  25877  limcco  25878  dvmptfsum  25960  lhop2  26000  lhop  26001  mdegcl  26052  elply2  26179  elplyd  26185  ply1term  26187  ply0  26191  plyaddlem1  26196  plymullem1  26197  plymullem  26199  mtest  26387  xrlimcnp  26950  jensen  26970  fsumharmonic  26993  chtdif  27139  lgsdir2lem3  27308  lgsquadlem2  27362  dchrisumlem2  27471  dchrisum0lem1b  27496  dchrisum0lem1  27497  pntrlog2bndlem6  27564  pntlemf  27586  nosupinfsep  27714  noetasuplem4  27718  noetalem1  27723  cofcutrtime  27937  addsuniflem  28011  addbday  28028  negsval  28035  mulsproplem12  28137  mulsproplem13  28138  mulsproplem14  28139  mulsuniflem  28159  mulsass  28176  precsexlem10  28226  bdayn0p1  28379  shsleji  31459  shsval2i  31476  ssjo  31536  sshhococi  31635  symgcom  33164  elrgspnsubrunlem1  33328  elrgspnsubrunlem2  33329  elrspunsn  33512  idlsrgtset  33591  vieta  33764  rtelextdg2  33911  constrextdg2lem  33932  esumsplit  34237  measun  34395  aean  34428  sxbrsigalem2  34470  bnj970  35129  bnj1137  35177  subfacp1lem2a  35408  subfacp1lem3  35410  subfacp1lem5  35412  erdszelem8  35426  kur14lem7  35440  cvmliftlem10  35522  mrsubvr  35739  refssfne  36586  topjoin  36593  tailf  36603  ttcuniun  36738  ttciunun  36739  bj-unrab  37279  bj-2upln1upl  37377  bj-ccinftyssccbar  37578  imadifss  37962  finixpnum  37972  matunitlindflem1  37983  mblfinlem4  38027  prdsbnd  38160  heibor1lem  38176  sspadd2  40308  pclfinN  40392  dochdmj1  41882  mzpcompact2lem  43200  eldioph2  43211  eldioph4b  43256  ttac  43481  pwssplit4  43534  isnumbasgrplem2  43549  isnumbasabl  43551  dfacbasgrp  43553  algsca  43622  algvsca  43623  fiuneneq  43637  tfsconcatrnss12  43794  rclexi  44059  rtrclex  44061  trclubgNEW  44062  trclexi  44064  rtrclexi  44065  cnvrcl0  44069  cnvtrcl0  44070  dfrtrcl5  44073  trrelsuperrel2dg  44115  dfrcl2  44118  relexp0a  44160  relexpaddss  44162  trclimalb2  44170  frege109d  44201  frege131d  44208  isotone1  44492  grumnudlem  44729  rnwf  45410  iblsplit  46409  fourierdlem46  46595  sge0resplit  46849  sge0split  46852  sge0splitmpt  46854  sge0xaddlem1  46876  sbgoldbo  48278  dfnbgrss  48343  gsumsplit2f  48671  setrec1  50181  elpglem2  50202