Theorem ssun2 4125

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 4124	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4105	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3979	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-un 3904  df-ss 3916

This theorem is used by:  ssun4  4127  elun2  4129  nsspssun  4214  unv  4349  un00  4357  pwunss  4575  snsspr2  4776  snsstp3  4779  imadifssran  6197  fvrn0  6906  riotassuni  7410  ovima0  7593  unexb  7748  difex2  7759  rnexg  7899  xpord2indlem  8145  xpord3inddlem  8152  fnsuppres  8189  brtpos0  8231  frrlem14  8298  oaabs2  8637  domunsncan  9075  mapunen  9144  ac6sfi  9254  unfir  9278  domunfican  9291  iunfi  9310  elfiun  9400  dffi3  9401  hartogslem1  9514  unwdomg  9556  unxpwdom2  9560  unxpwdom  9561  trcl  9707  unwf  9792  rankunb  9832  r0weon  10015  infxpenlem  10016  alephfplem4  10110  dju1dif  10175  cdainflem  10190  infdju  10209  cfsuc  10259  fin1a2lem10  10411  axdc3lem4  10455  ttukeylem7  10517  fpwwe2lem12  10651  canthp1lem2  10662  gchac  10690  wunrn  10738  wunex2  10747  inar1  10784  pnfxr  11287  ltrelxr  11294  un0mulcl  12562  fzdifsuc  13639  seqexw  14081  hashbclem  14517  hashf1lem1  14520  ccatrn  14655  trclublem  15068  relexprng  15119  fsumsplit  15827  o1fsum  15900  incexclem  15925  fprodsplit  16053  vdwlem5  17077  vdwlem8  17080  ramcl2  17108  srnginvl  17398  lmodvsca  17414  ipssca  17425  ipsvsca  17426  ipsip  17427  phlvsca  17435  phlip  17436  odrngtset  17492  odrngle  17493  odrngds  17494  prdssca  17541  prdsvsca  17545  prdsip  17546  prdsle  17547  prdsds  17549  prdstset  17551  prdshom  17552  prdsco  17553  imasds  17599  imassca  17605  imasvsca  17606  imasip  17607  imastset  17608  imasle  17609  mreexexlemd  17732  mreexexlem2d  17733  mreexexlem3d  17734  drsdirfi  18393  ipolerval  18620  psdmrn  18661  dirge  18691  grpinvfval  19102  mulgfval  19192  gsumzsplit  20054  gsumsplit2  20056  gsumzunsnd  20083  gsum2dlem2  20098  dprdfadd  20149  dmdprdsplit2lem  20174  dmdprdsplit2  20175  dmdprdsplit  20176  dprdsplit  20177  ablfac1eulem  20201  pgpfaclem1  20210  gsumle  20272  lspun  21171  lbsextlem2  21346  lbsextlem3  21347  lbsextlem4  21348  cnfldcj  21594  cnfldtset  21595  cnfldle  21596  cnfldds  21597  cnfldunif  21598  psrsca  22162  psrvscafval  22163  mplsubglem  22213  mplcoe5  22256  opsrtoslem2  22272  matunitlindflem1  22901  ordtbas2  23416  ordtbas  23417  ordtopn1  23419  ordtopn2  23420  leordtval2  23437  icomnfordt  23441  iooordt  23442  perfcls  23590  uncmp  23628  fiuncmp  23629  2ndcdisj2  23683  comppfsc  23758  1stckgenlem  23779  1stckgen  23780  ptbasin  23803  ptbasfi  23807  dfac14lem  23843  dfac14  23844  ptuncnv  24033  ptunhmeo  24034  ptcmpfi  24039  fbun  24066  filconn  24109  isufil2  24134  ufprim  24135  fin1aufil  24158  flimclslem  24210  flimfnfcls  24254  tmdgsum  24321  tsmsgsum  24365  tsmssplit  24378  tsmsxplem1  24379  trust  24455  prdsdsf  24593  prdsmet  24596  prdsbl  24717  cnmpopc  25156  rrxmetlem  25635  rrxmet  25636  rrxdstprj1  25637  ovolctb2  25720  ovolfiniun  25729  finiunmbl  25772  volfiniun  25775  uniioombllem3  25813  uniioombllem4  25814  mbfres2  25873  itg2splitlem  25976  itg2split  25977  itgsplit  26063  limcvallem  26098  ellimc2  26104  limccnp  26118  limccnp2  26119  limcco  26120  dvmptfsum  26202  lhop2  26242  lhop  26243  mdegcl  26294  elply2  26421  elplyd  26427  ply1term  26429  ply0  26433  plyaddlem1  26439  plymullem1  26440  plymullem  26442  mtest  26640  xrlimcnp  27205  jensen  27225  fsumharmonic  27248  chtdif  27394  lgsdir2lem3  27563  lgsquadlem2  27617  dchrisumlem2  27726  dchrisum0lem1b  27751  dchrisum0lem1  27752  pntrlog2bndlem6  27819  pntlemf  27841  nosupinfsep  27968  noetasuplem4  27972  noetalem1  27977  cofcutrtime  28192  addsuniflem  28266  addbday  28283  negsval  28290  mulsproplem12  28392  mulsproplem13  28393  mulsproplem14  28394  mulsuniflem  28414  mulsass  28431  precsexlem10  28481  bdayn0p1  28634  shsleji  31851  shsval2i  31868  ssjo  31928  sshhococi  32027  symgcom  33523  elrgspnsubrunlem1  33687  elrgspnsubrunlem2  33688  elrspunsn  33857  idlsrgtset  33918  vieta  34090  rtelextdg2  34237  constrextdg2lem  34258  esumsplit  34563  measun  34722  aean  34755  sxbrsigalem2  34797  bnj970  35456  bnj1137  35504  subfacp1lem2a  35759  subfacp1lem3  35761  subfacp1lem5  35763  erdszelem8  35777  kur14lem7  35791  cvmliftlem10  35873  mrsubvr  36090  refssfne  36977  topjoin  36984  tailf  36994  ttcuniun  37129  ttciunun  37130  bj-unrab  37670  bj-2upln1upl  37768  bj-ccinftyssccbar  37970  imadifss  38354  finixpnum  38359  mblfinlem4  38409  prdsbnd  38543  heibor1lem  38559  sspadd2  40689  pclfinN  40773  dochdmj1  42263  mzpcompact2lem  43596  eldioph2  43607  eldioph4b  43652  ttac  43877  pwssplit4  43930  isnumbasgrplem2  43945  isnumbasabl  43947  dfacbasgrp  43949  algsca  44018  algvsca  44019  fiuneneq  44033  tfsconcatrnss12  44190  rclexi  44455  rtrclex  44457  trclubgNEW  44458  trclexi  44460  rtrclexi  44461  cnvrcl0  44465  cnvtrcl0  44466  dfrtrcl5  44469  trrelsuperrel2dg  44511  dfrcl2  44514  relexp0a  44556  relexpaddss  44558  trclimalb2  44566  frege109d  44597  frege131d  44604  isotone1  44888  grumnudlem  45109  rnwf  45789  iblsplit  46794  fourierdlem46  46980  sge0resplit  47234  sge0split  47237  sge0splitmpt  47239  sge0xaddlem1  47261  wrddun  47717  chndun  47722  chnrun  47727  sbgoldbo  48703  dfnbgrss  48768  gsumsplit2f  49095  setrec1  50617  elpglem2  50638