Theorem ssun2 4161

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 4160	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4140	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4014	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3931   ⊆ wss 3933

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1794  ax-4 1808  ax-5 1909  ax-6 1966  ax-7 2006  ax-8 2109  ax-9 2117  ax-ext 2706

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1542  df-ex 1779  df-sb 2064  df-clab 2713  df-cleq 2726  df-clel 2808  df-v 3466  df-un 3938  df-ss 3950

This theorem is referenced by:  ssun4  4163  elun2  4165  nsspssun  4250  unv  4381  un00  4427  pwunss  4600  snsspr2  4797  snsstp3  4800  fvrn0  6917  riotassuni  7411  ovima0  7595  unexb  7750  unexbOLD  7751  difex2  7763  rnexg  7907  xpord2indlem  8155  xpord3inddlem  8162  fnsuppres  8199  brtpos0  8241  frrlem14  8307  wfrlem16OLD  8347  oaabs2  8670  domunsncan  9095  mapunen  9169  ac6sfi  9303  unfir  9329  domunfican  9344  iunfi  9366  elfiun  9453  dffi3  9454  hartogslem1  9565  unwdomg  9607  unxpwdom2  9611  unxpwdom  9612  trcl  9751  unwf  9833  rankunb  9873  r0weon  10035  infxpenlem  10036  alephfplem4  10130  dju1dif  10196  cdainflem  10211  infdju  10230  cfsuc  10280  fin1a2lem10  10432  axdc3lem4  10476  ttukeylem7  10538  fpwwe2lem12  10665  canthp1lem2  10676  gchac  10704  wunrn  10752  wunex2  10761  inar1  10798  pnfxr  11298  ltrelxr  11305  un0mulcl  12544  fzdifsuc  13607  seqexw  14041  hashbclem  14474  hashf1lem1  14477  ccatrn  14610  trclublem  15017  relexprng  15068  fsumsplit  15760  o1fsum  15832  incexclem  15855  fprodsplit  15985  vdwlem5  17006  vdwlem8  17009  ramcl2  17037  srnginvl  17334  lmodvsca  17350  ipssca  17361  ipsvsca  17362  ipsip  17363  phlvsca  17371  phlip  17372  odrngtset  17428  odrngle  17429  odrngds  17430  prdssca  17477  prdsvsca  17481  prdsip  17482  prdsle  17483  prdsds  17485  prdstset  17487  prdshom  17488  prdsco  17489  imasds  17534  imassca  17540  imasvsca  17541  imasip  17542  imastset  17543  imasle  17544  mreexexlemd  17663  mreexexlem2d  17664  mreexexlem3d  17665  drsdirfi  18326  ipolerval  18551  psdmrn  18592  dirge  18622  grpinvfval  18970  mulgfval  19061  gsumzsplit  19918  gsumsplit2  19920  gsumzunsnd  19947  gsum2dlem2  19962  dprdfadd  20013  dmdprdsplit2lem  20038  dmdprdsplit2  20039  dmdprdsplit  20040  dprdsplit  20041  ablfac1eulem  20065  pgpfaclem1  20074  lspun  20958  lbsextlem2  21134  lbsextlem3  21135  lbsextlem4  21136  cnfldcj  21340  cnfldtset  21341  cnfldle  21342  cnfldds  21343  cnfldunif  21344  cnfldcjOLD  21353  cnfldtsetOLD  21354  cnfldleOLD  21355  cnflddsOLD  21356  cnfldunifOLD  21357  psrsca  21934  psrvscafval  21935  mplsubglem  21986  mplcoe5  22025  opsrtoslem2  22047  ordtbas2  23164  ordtbas  23165  ordtopn1  23167  ordtopn2  23168  leordtval2  23185  icomnfordt  23189  iooordt  23190  perfcls  23338  uncmp  23376  fiuncmp  23377  2ndcdisj2  23430  comppfsc  23505  1stckgenlem  23526  1stckgen  23527  ptbasin  23550  ptbasfi  23554  dfac14lem  23590  dfac14  23591  ptuncnv  23780  ptunhmeo  23781  ptcmpfi  23786  fbun  23813  filconn  23856  isufil2  23881  ufprim  23882  fin1aufil  23905  flimclslem  23957  flimfnfcls  24001  tmdgsum  24068  tsmsgsum  24112  tsmssplit  24125  tsmsxplem1  24126  trust  24203  prdsdsf  24341  prdsmet  24344  prdsbl  24467  cnmpopc  24910  rrxmetlem  25396  rrxmet  25397  rrxdstprj1  25398  ovolctb2  25482  ovolfiniun  25491  finiunmbl  25534  volfiniun  25537  uniioombllem3  25575  uniioombllem4  25576  mbfres2  25635  itg2splitlem  25738  itg2split  25739  itgsplit  25826  limcvallem  25861  ellimc2  25867  limccnp  25881  limccnp2  25882  limcco  25883  dvmptfsum  25968  lhop2  26009  lhop  26010  mdegcl  26063  elply2  26190  elplyd  26196  ply1term  26198  ply0  26202  plyaddlem1  26207  plymullem1  26208  plymullem  26210  mtest  26402  xrlimcnp  26966  jensen  26987  fsumharmonic  27010  chtdif  27156  lgsdir2lem3  27326  lgsquadlem2  27380  dchrisumlem2  27489  dchrisum0lem1b  27514  dchrisum0lem1  27515  pntrlog2bndlem6  27582  pntlemf  27604  nosupinfsep  27732  noetasuplem4  27736  noetalem1  27741  cofcutrtime  27916  addsuniflem  27989  addsbday  28005  negsval  28012  mulsproplem12  28108  mulsproplem13  28109  mulsproplem14  28110  mulsuniflem  28130  mulsass  28147  precsexlem10  28195  shsleji  31336  shsval2i  31353  ssjo  31413  sshhococi  31512  gsumle  33047  symgcom  33049  elrgspnsubrunlem1  33197  elrgspnsubrunlem2  33198  elrspunsn  33398  idlsrgtset  33477  rtelextdg2  33709  constrextdg2lem  33730  esumsplit  33995  measun  34153  aean  34186  sxbrsigalem2  34229  bnj970  34902  bnj1137  34950  subfacp1lem2a  35126  subfacp1lem3  35128  subfacp1lem5  35130  erdszelem8  35144  kur14lem7  35158  cvmliftlem10  35240  mrsubvr  35457  refssfne  36300  topjoin  36307  tailf  36317  bj-unrab  36868  bj-2upln1upl  36966  bj-ccinftyssccbar  37160  imadifss  37543  finixpnum  37553  matunitlindflem1  37564  mblfinlem4  37608  prdsbnd  37741  heibor1lem  37757  sspadd2  39759  pclfinN  39843  dochdmj1  41333  mzpcompact2lem  42707  eldioph2  42718  eldioph4b  42767  ttac  42993  pwssplit4  43046  isnumbasgrplem2  43061  isnumbasabl  43063  dfacbasgrp  43065  algsca  43134  algvsca  43135  fiuneneq  43149  tfsconcatrnss12  43307  rclexi  43573  rtrclex  43575  trclubgNEW  43576  trclexi  43578  rtrclexi  43579  cnvrcl0  43583  cnvtrcl0  43584  dfrtrcl5  43587  trrelsuperrel2dg  43629  dfrcl2  43632  relexp0a  43674  relexpaddss  43676  trclimalb2  43684  frege109d  43715  frege131d  43722  isotone1  44006  grumnudlem  44249  rnwf  44928  iblsplit  45926  fourierdlem46  46112  sge0resplit  46366  sge0split  46369  sge0splitmpt  46371  sge0xaddlem1  46393  sbgoldbo  47720  dfnbgrss  47784  gsumsplit2f  48042  setrec1  49206  elpglem2  49227