Theorem ssun2 4133

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 4132	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4112	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3984	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3901   ⊆ wss 3903

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-un 3908  df-ss 3920

This theorem is referenced by:  ssun4  4135  elun2  4137  nsspssun  4222  unv  4353  un00  4399  pwunss  4574  snsspr2  4773  snsstp3  4776  fvrn0  6870  riotassuni  7365  ovima0  7547  unexb  7702  unexbOLD  7703  difex2  7715  rnexg  7854  xpord2indlem  8099  xpord3inddlem  8106  fnsuppres  8143  brtpos0  8185  frrlem14  8251  oaabs2  8587  domunsncan  9017  mapunen  9086  ac6sfi  9196  unfir  9220  domunfican  9234  iunfi  9255  elfiun  9345  dffi3  9346  hartogslem1  9459  unwdomg  9501  unxpwdom2  9505  unxpwdom  9506  trcl  9649  unwf  9734  rankunb  9774  r0weon  9934  infxpenlem  9935  alephfplem4  10029  dju1dif  10095  cdainflem  10110  infdju  10129  cfsuc  10179  fin1a2lem10  10331  axdc3lem4  10375  ttukeylem7  10437  fpwwe2lem12  10565  canthp1lem2  10576  gchac  10604  wunrn  10652  wunex2  10661  inar1  10698  pnfxr  11198  ltrelxr  11205  un0mulcl  12447  fzdifsuc  13512  seqexw  13952  hashbclem  14387  hashf1lem1  14390  ccatrn  14525  trclublem  14930  relexprng  14981  fsumsplit  15676  o1fsum  15748  incexclem  15771  fprodsplit  15901  vdwlem5  16925  vdwlem8  16928  ramcl2  16956  srnginvl  17245  lmodvsca  17261  ipssca  17272  ipsvsca  17273  ipsip  17274  phlvsca  17282  phlip  17283  odrngtset  17339  odrngle  17340  odrngds  17341  prdssca  17388  prdsvsca  17392  prdsip  17393  prdsle  17394  prdsds  17396  prdstset  17398  prdshom  17399  prdsco  17400  imasds  17446  imassca  17452  imasvsca  17453  imasip  17454  imastset  17455  imasle  17456  mreexexlemd  17579  mreexexlem2d  17580  mreexexlem3d  17581  drsdirfi  18240  ipolerval  18467  psdmrn  18508  dirge  18538  grpinvfval  18920  mulgfval  19011  gsumzsplit  19868  gsumsplit2  19870  gsumzunsnd  19897  gsum2dlem2  19912  dprdfadd  19963  dmdprdsplit2lem  19988  dmdprdsplit2  19989  dmdprdsplit  19990  dprdsplit  19991  ablfac1eulem  20015  pgpfaclem1  20024  gsumle  20086  lspun  20950  lbsextlem2  21126  lbsextlem3  21127  lbsextlem4  21128  cnfldcj  21330  cnfldtset  21331  cnfldle  21332  cnfldds  21333  cnfldunif  21334  cnfldcjOLD  21343  cnfldtsetOLD  21344  cnfldleOLD  21345  cnflddsOLD  21346  cnfldunifOLD  21347  psrsca  21915  psrvscafval  21916  mplsubglem  21966  mplcoe5  22007  opsrtoslem2  22023  ordtbas2  23147  ordtbas  23148  ordtopn1  23150  ordtopn2  23151  leordtval2  23168  icomnfordt  23172  iooordt  23173  perfcls  23321  uncmp  23359  fiuncmp  23360  2ndcdisj2  23413  comppfsc  23488  1stckgenlem  23509  1stckgen  23510  ptbasin  23533  ptbasfi  23537  dfac14lem  23573  dfac14  23574  ptuncnv  23763  ptunhmeo  23764  ptcmpfi  23769  fbun  23796  filconn  23839  isufil2  23864  ufprim  23865  fin1aufil  23888  flimclslem  23940  flimfnfcls  23984  tmdgsum  24051  tsmsgsum  24095  tsmssplit  24108  tsmsxplem1  24109  trust  24185  prdsdsf  24323  prdsmet  24326  prdsbl  24447  cnmpopc  24890  rrxmetlem  25375  rrxmet  25376  rrxdstprj1  25377  ovolctb2  25461  ovolfiniun  25470  finiunmbl  25513  volfiniun  25516  uniioombllem3  25554  uniioombllem4  25555  mbfres2  25614  itg2splitlem  25717  itg2split  25718  itgsplit  25805  limcvallem  25840  ellimc2  25846  limccnp  25860  limccnp2  25861  limcco  25862  dvmptfsum  25947  lhop2  25988  lhop  25989  mdegcl  26042  elply2  26169  elplyd  26175  ply1term  26177  ply0  26181  plyaddlem1  26186  plymullem1  26187  plymullem  26189  mtest  26381  xrlimcnp  26946  jensen  26967  fsumharmonic  26990  chtdif  27136  lgsdir2lem3  27306  lgsquadlem2  27360  dchrisumlem2  27469  dchrisum0lem1b  27494  dchrisum0lem1  27495  pntrlog2bndlem6  27562  pntlemf  27584  nosupinfsep  27712  noetasuplem4  27716  noetalem1  27721  cofcutrtime  27935  addsuniflem  28009  addbday  28026  negsval  28033  mulsproplem12  28135  mulsproplem13  28136  mulsproplem14  28137  mulsuniflem  28157  mulsass  28174  precsexlem10  28224  bdayn0p1  28377  shsleji  31457  shsval2i  31474  ssjo  31534  sshhococi  31633  symgcom  33176  elrgspnsubrunlem1  33340  elrgspnsubrunlem2  33341  elrspunsn  33521  idlsrgtset  33600  vieta  33756  rtelextdg2  33904  constrextdg2lem  33925  esumsplit  34230  measun  34388  aean  34421  sxbrsigalem2  34463  bnj970  35122  bnj1137  35170  subfacp1lem2a  35393  subfacp1lem3  35395  subfacp1lem5  35397  erdszelem8  35411  kur14lem7  35425  cvmliftlem10  35507  mrsubvr  35724  refssfne  36571  topjoin  36578  tailf  36588  bj-unrab  37171  bj-2upln1upl  37269  bj-ccinftyssccbar  37470  imadifss  37843  finixpnum  37853  matunitlindflem1  37864  mblfinlem4  37908  prdsbnd  38041  heibor1lem  38057  sspadd2  40189  pclfinN  40273  dochdmj1  41763  mzpcompact2lem  43105  eldioph2  43116  eldioph4b  43165  ttac  43390  pwssplit4  43443  isnumbasgrplem2  43458  isnumbasabl  43460  dfacbasgrp  43462  algsca  43531  algvsca  43532  fiuneneq  43546  tfsconcatrnss12  43703  rclexi  43968  rtrclex  43970  trclubgNEW  43971  trclexi  43973  rtrclexi  43974  cnvrcl0  43978  cnvtrcl0  43979  dfrtrcl5  43982  trrelsuperrel2dg  44024  dfrcl2  44027  relexp0a  44069  relexpaddss  44071  trclimalb2  44079  frege109d  44110  frege131d  44117  isotone1  44401  grumnudlem  44638  rnwf  45319  iblsplit  46321  fourierdlem46  46507  sge0resplit  46761  sge0split  46764  sge0splitmpt  46766  sge0xaddlem1  46788  sbgoldbo  48144  dfnbgrss  48209  gsumsplit2f  48537  setrec1  50047  elpglem2  50068