Theorem ssun2 4138

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 4137	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4117	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3992	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3909   ⊆ wss 3911

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3446  df-un 3916  df-ss 3928

This theorem is referenced by:  ssun4  4140  elun2  4142  nsspssun  4227  unv  4358  un00  4404  pwunss  4577  snsspr2  4775  snsstp3  4778  fvrn0  6870  riotassuni  7366  ovima0  7548  unexb  7703  unexbOLD  7704  difex2  7716  rnexg  7858  xpord2indlem  8103  xpord3inddlem  8110  fnsuppres  8147  brtpos0  8189  frrlem14  8255  oaabs2  8590  domunsncan  9018  mapunen  9087  ac6sfi  9207  unfir  9233  domunfican  9248  iunfi  9270  elfiun  9357  dffi3  9358  hartogslem1  9471  unwdomg  9513  unxpwdom2  9517  unxpwdom  9518  trcl  9657  unwf  9739  rankunb  9779  r0weon  9941  infxpenlem  9942  alephfplem4  10036  dju1dif  10102  cdainflem  10117  infdju  10136  cfsuc  10186  fin1a2lem10  10338  axdc3lem4  10382  ttukeylem7  10444  fpwwe2lem12  10571  canthp1lem2  10582  gchac  10610  wunrn  10658  wunex2  10667  inar1  10704  pnfxr  11204  ltrelxr  11211  un0mulcl  12452  fzdifsuc  13521  seqexw  13958  hashbclem  14393  hashf1lem1  14396  ccatrn  14530  trclublem  14937  relexprng  14988  fsumsplit  15683  o1fsum  15755  incexclem  15778  fprodsplit  15908  vdwlem5  16932  vdwlem8  16935  ramcl2  16963  srnginvl  17252  lmodvsca  17268  ipssca  17279  ipsvsca  17280  ipsip  17281  phlvsca  17289  phlip  17290  odrngtset  17346  odrngle  17347  odrngds  17348  prdssca  17395  prdsvsca  17399  prdsip  17400  prdsle  17401  prdsds  17403  prdstset  17405  prdshom  17406  prdsco  17407  imasds  17452  imassca  17458  imasvsca  17459  imasip  17460  imastset  17461  imasle  17462  mreexexlemd  17581  mreexexlem2d  17582  mreexexlem3d  17583  drsdirfi  18242  ipolerval  18467  psdmrn  18508  dirge  18538  grpinvfval  18886  mulgfval  18977  gsumzsplit  19833  gsumsplit2  19835  gsumzunsnd  19862  gsum2dlem2  19877  dprdfadd  19928  dmdprdsplit2lem  19953  dmdprdsplit2  19954  dmdprdsplit  19955  dprdsplit  19956  ablfac1eulem  19980  pgpfaclem1  19989  lspun  20869  lbsextlem2  21045  lbsextlem3  21046  lbsextlem4  21047  cnfldcj  21249  cnfldtset  21250  cnfldle  21251  cnfldds  21252  cnfldunif  21253  cnfldcjOLD  21262  cnfldtsetOLD  21263  cnfldleOLD  21264  cnflddsOLD  21265  cnfldunifOLD  21266  psrsca  21832  psrvscafval  21833  mplsubglem  21884  mplcoe5  21923  opsrtoslem2  21939  ordtbas2  23054  ordtbas  23055  ordtopn1  23057  ordtopn2  23058  leordtval2  23075  icomnfordt  23079  iooordt  23080  perfcls  23228  uncmp  23266  fiuncmp  23267  2ndcdisj2  23320  comppfsc  23395  1stckgenlem  23416  1stckgen  23417  ptbasin  23440  ptbasfi  23444  dfac14lem  23480  dfac14  23481  ptuncnv  23670  ptunhmeo  23671  ptcmpfi  23676  fbun  23703  filconn  23746  isufil2  23771  ufprim  23772  fin1aufil  23795  flimclslem  23847  flimfnfcls  23891  tmdgsum  23958  tsmsgsum  24002  tsmssplit  24015  tsmsxplem1  24016  trust  24093  prdsdsf  24231  prdsmet  24234  prdsbl  24355  cnmpopc  24798  rrxmetlem  25283  rrxmet  25284  rrxdstprj1  25285  ovolctb2  25369  ovolfiniun  25378  finiunmbl  25421  volfiniun  25424  uniioombllem3  25462  uniioombllem4  25463  mbfres2  25522  itg2splitlem  25625  itg2split  25626  itgsplit  25713  limcvallem  25748  ellimc2  25754  limccnp  25768  limccnp2  25769  limcco  25770  dvmptfsum  25855  lhop2  25896  lhop  25897  mdegcl  25950  elply2  26077  elplyd  26083  ply1term  26085  ply0  26089  plyaddlem1  26094  plymullem1  26095  plymullem  26097  mtest  26289  xrlimcnp  26854  jensen  26875  fsumharmonic  26898  chtdif  27044  lgsdir2lem3  27214  lgsquadlem2  27268  dchrisumlem2  27377  dchrisum0lem1b  27402  dchrisum0lem1  27403  pntrlog2bndlem6  27470  pntlemf  27492  nosupinfsep  27620  noetasuplem4  27624  noetalem1  27629  cofcutrtime  27811  addsuniflem  27884  addsbday  27900  negsval  27907  mulsproplem12  28006  mulsproplem13  28007  mulsproplem14  28008  mulsuniflem  28028  mulsass  28045  precsexlem10  28094  bdayn0p1  28234  shsleji  31272  shsval2i  31289  ssjo  31349  sshhococi  31448  gsumle  33011  symgcom  33013  elrgspnsubrunlem1  33171  elrgspnsubrunlem2  33172  elrspunsn  33373  idlsrgtset  33452  rtelextdg2  33690  constrextdg2lem  33711  esumsplit  34016  measun  34174  aean  34207  sxbrsigalem2  34250  bnj970  34910  bnj1137  34958  subfacp1lem2a  35140  subfacp1lem3  35142  subfacp1lem5  35144  erdszelem8  35158  kur14lem7  35172  cvmliftlem10  35254  mrsubvr  35471  refssfne  36319  topjoin  36326  tailf  36336  bj-unrab  36887  bj-2upln1upl  36985  bj-ccinftyssccbar  37179  imadifss  37562  finixpnum  37572  matunitlindflem1  37583  mblfinlem4  37627  prdsbnd  37760  heibor1lem  37776  sspadd2  39783  pclfinN  39867  dochdmj1  41357  mzpcompact2lem  42712  eldioph2  42723  eldioph4b  42772  ttac  42998  pwssplit4  43051  isnumbasgrplem2  43066  isnumbasabl  43068  dfacbasgrp  43070  algsca  43139  algvsca  43140  fiuneneq  43154  tfsconcatrnss12  43311  rclexi  43577  rtrclex  43579  trclubgNEW  43580  trclexi  43582  rtrclexi  43583  cnvrcl0  43587  cnvtrcl0  43588  dfrtrcl5  43591  trrelsuperrel2dg  43633  dfrcl2  43636  relexp0a  43678  relexpaddss  43680  trclimalb2  43688  frege109d  43719  frege131d  43726  isotone1  44010  grumnudlem  44247  rnwf  44929  iblsplit  45937  fourierdlem46  46123  sge0resplit  46377  sge0split  46380  sge0splitmpt  46382  sge0xaddlem1  46404  sbgoldbo  47761  dfnbgrss  47825  gsumsplit2f  48141  setrec1  49653  elpglem2  49674