Theorem ssun2 4103

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 4102	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4083	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3953	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 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-or 844  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-un 3888  df-in 3890  df-ss 3900

This theorem is referenced by:  ssun4  4105  elun2  4107  nsspssun  4188  unv  4326  un00  4373  pwunss  4550  snsspr2  4745  snsstp3  4748  fvrn0  6784  riotassuni  7253  ovima0  7429  unexb  7576  difex2  7588  rnexg  7725  fnsuppres  7978  brtpos0  8020  frrlem14  8086  wfrlem16OLD  8126  oaabs2  8439  domunsncan  8812  mapunen  8882  ac6sfi  8988  unfir  9012  domunfican  9017  iunfi  9037  elfiun  9119  dffi3  9120  hartogslem1  9231  unwdomg  9273  unxpwdom2  9277  unxpwdom  9278  trcl  9417  unwf  9499  rankunb  9539  r0weon  9699  infxpenlem  9700  alephfplem4  9794  dju1dif  9859  cdainflem  9874  infdju  9895  cfsuc  9944  fin1a2lem10  10096  axdc3lem4  10140  ttukeylem7  10202  fpwwe2lem12  10329  canthp1lem2  10340  gchac  10368  wunrn  10416  wunex2  10425  inar1  10462  pnfxr  10960  ltrelxr  10967  un0mulcl  12197  fzdifsuc  13245  seqexw  13665  hashbclem  14092  hashf1lem1  14096  hashf1lem1OLD  14097  ccatrn  14222  trclublem  14634  relexprng  14685  fsumsplit  15381  o1fsum  15453  incexclem  15476  fprodsplit  15604  vdwlem5  16614  vdwlem8  16617  ramcl2  16645  srnginvl  16949  lmodvsca  16965  ipssca  16975  ipsvsca  16976  ipsip  16977  phlvsca  16985  phlip  16986  odrngtset  17036  odrngle  17037  odrngds  17038  prdssca  17084  prdsvsca  17088  prdsip  17089  prdsle  17090  prdsds  17092  prdstset  17094  prdshom  17095  prdsco  17096  imasds  17141  imassca  17147  imasvsca  17148  imasip  17149  imastset  17150  imasle  17151  mreexexlemd  17270  mreexexlem2d  17271  mreexexlem3d  17272  drsdirfi  17938  ipolerval  18165  psdmrn  18206  dirge  18236  grpinvfval  18533  mulgfval  18617  gsumzsplit  19443  gsumsplit2  19445  gsumzunsnd  19472  gsum2dlem2  19487  dprdfadd  19538  dmdprdsplit2lem  19563  dmdprdsplit2  19564  dmdprdsplit  19565  dprdsplit  19566  ablfac1eulem  19590  pgpfaclem1  19599  lspun  20164  lbsextlem2  20336  lbsextlem3  20337  lbsextlem4  20338  cnfldcj  20517  cnfldtset  20518  cnfldle  20519  cnfldds  20520  cnfldunif  20521  psrbagaddclOLD  21042  psrsca  21068  psrvscafval  21069  mplsubglem  21115  mplcoe5  21151  opsrtoslem2  21173  ordtbas2  22250  ordtbas  22251  ordtopn1  22253  ordtopn2  22254  leordtval2  22271  icomnfordt  22275  iooordt  22276  perfcls  22424  uncmp  22462  fiuncmp  22463  2ndcdisj2  22516  comppfsc  22591  1stckgenlem  22612  1stckgen  22613  ptbasin  22636  ptbasfi  22640  dfac14lem  22676  dfac14  22677  ptuncnv  22866  ptunhmeo  22867  ptcmpfi  22872  fbun  22899  filconn  22942  isufil2  22967  ufprim  22968  fin1aufil  22991  flimclslem  23043  flimfnfcls  23087  tmdgsum  23154  tsmsgsum  23198  tsmssplit  23211  tsmsxplem1  23212  trust  23289  prdsdsf  23428  prdsmet  23431  prdsbl  23553  cnmpopc  23997  rrxmetlem  24476  rrxmet  24477  rrxdstprj1  24478  ovolctb2  24561  ovolfiniun  24570  finiunmbl  24613  volfiniun  24616  uniioombllem3  24654  uniioombllem4  24655  mbfres2  24714  itg2splitlem  24818  itg2split  24819  itgsplit  24905  limcvallem  24940  ellimc2  24946  limccnp  24960  limccnp2  24961  limcco  24962  dvmptfsum  25044  lhop2  25084  lhop  25085  mdegcl  25139  elply2  25262  elplyd  25268  ply1term  25270  ply0  25274  plyaddlem1  25279  plymullem1  25280  plymullem  25282  mtest  25468  xrlimcnp  26023  jensen  26043  fsumharmonic  26066  chtdif  26212  lgsdir2lem3  26380  lgsquadlem2  26434  dchrisumlem2  26543  dchrisum0lem1b  26568  dchrisum0lem1  26569  pntrlog2bndlem6  26636  pntlemf  26658  shsleji  29633  shsval2i  29650  ssjo  29710  sshhococi  29809  gsumle  31252  symgcom  31254  idlsrgtset  31555  esumsplit  31921  measun  32079  aean  32112  sxbrsigalem2  32153  bnj970  32827  bnj1137  32875  subfacp1lem2a  33042  subfacp1lem3  33044  subfacp1lem5  33046  erdszelem8  33060  kur14lem7  33074  cvmliftlem10  33156  mrsubvr  33373  xpord2ind  33721  xpord3ind  33727  nosupinfsep  33862  noetasuplem4  33866  noetalem1  33871  cofcutrtime  34020  negsval  34050  refssfne  34474  topjoin  34481  tailf  34491  bj-unrab  35041  bj-2upln1upl  35141  bj-ccinftyssccbar  35316  imadifss  35679  finixpnum  35689  matunitlindflem1  35700  mblfinlem4  35744  prdsbnd  35878  heibor1lem  35894  sspadd2  37757  pclfinN  37841  dochdmj1  39331  mzpcompact2lem  40489  eldioph2  40500  eldioph4b  40549  ttac  40774  pwssplit4  40830  isnumbasgrplem2  40845  isnumbasabl  40847  dfacbasgrp  40849  algsca  40922  algvsca  40923  fiuneneq  40938  rclexi  41112  rtrclex  41114  trclubgNEW  41115  trclexi  41117  rtrclexi  41118  cnvrcl0  41122  cnvtrcl0  41123  dfrtrcl5  41126  trrelsuperrel2dg  41168  dfrcl2  41171  relexp0a  41213  relexpaddss  41215  trclimalb2  41223  frege109d  41254  frege131d  41261  isotone1  41547  grumnudlem  41792  iblsplit  43397  fourierdlem46  43583  sge0resplit  43834  sge0split  43837  sge0splitmpt  43839  sge0xaddlem1  43861  sbgoldbo  45127  gsumsplit2f  45262  setrec1  46283  elpglem2  46303