Theorem ssun2 4130

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 4129	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4109	. 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 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 3438  df-un 3908  df-ss 3920

This theorem is referenced by:  ssun4  4132  elun2  4134  nsspssun  4219  unv  4350  un00  4396  pwunss  4569  snsspr2  4766  snsstp3  4769  fvrn0  6850  riotassuni  7346  ovima0  7528  unexb  7683  unexbOLD  7684  difex2  7696  rnexg  7835  xpord2indlem  8080  xpord3inddlem  8087  fnsuppres  8124  brtpos0  8166  frrlem14  8232  oaabs2  8567  domunsncan  8994  mapunen  9063  ac6sfi  9173  unfir  9197  domunfican  9211  iunfi  9233  elfiun  9320  dffi3  9321  hartogslem1  9434  unwdomg  9476  unxpwdom2  9480  unxpwdom  9481  trcl  9624  unwf  9706  rankunb  9746  r0weon  9906  infxpenlem  9907  alephfplem4  10001  dju1dif  10067  cdainflem  10082  infdju  10101  cfsuc  10151  fin1a2lem10  10303  axdc3lem4  10347  ttukeylem7  10409  fpwwe2lem12  10536  canthp1lem2  10547  gchac  10575  wunrn  10623  wunex2  10632  inar1  10669  pnfxr  11169  ltrelxr  11176  un0mulcl  12418  fzdifsuc  13487  seqexw  13924  hashbclem  14359  hashf1lem1  14362  ccatrn  14496  trclublem  14902  relexprng  14953  fsumsplit  15648  o1fsum  15720  incexclem  15743  fprodsplit  15873  vdwlem5  16897  vdwlem8  16900  ramcl2  16928  srnginvl  17217  lmodvsca  17233  ipssca  17244  ipsvsca  17245  ipsip  17246  phlvsca  17254  phlip  17255  odrngtset  17311  odrngle  17312  odrngds  17313  prdssca  17360  prdsvsca  17364  prdsip  17365  prdsle  17366  prdsds  17368  prdstset  17370  prdshom  17371  prdsco  17372  imasds  17417  imassca  17423  imasvsca  17424  imasip  17425  imastset  17426  imasle  17427  mreexexlemd  17550  mreexexlem2d  17551  mreexexlem3d  17552  drsdirfi  18211  ipolerval  18438  psdmrn  18479  dirge  18509  grpinvfval  18857  mulgfval  18948  gsumzsplit  19806  gsumsplit2  19808  gsumzunsnd  19835  gsum2dlem2  19850  dprdfadd  19901  dmdprdsplit2lem  19926  dmdprdsplit2  19927  dmdprdsplit  19928  dprdsplit  19929  ablfac1eulem  19953  pgpfaclem1  19962  gsumle  20024  lspun  20890  lbsextlem2  21066  lbsextlem3  21067  lbsextlem4  21068  cnfldcj  21270  cnfldtset  21271  cnfldle  21272  cnfldds  21273  cnfldunif  21274  cnfldcjOLD  21283  cnfldtsetOLD  21284  cnfldleOLD  21285  cnflddsOLD  21286  cnfldunifOLD  21287  psrsca  21854  psrvscafval  21855  mplsubglem  21906  mplcoe5  21945  opsrtoslem2  21961  ordtbas2  23076  ordtbas  23077  ordtopn1  23079  ordtopn2  23080  leordtval2  23097  icomnfordt  23101  iooordt  23102  perfcls  23250  uncmp  23288  fiuncmp  23289  2ndcdisj2  23342  comppfsc  23417  1stckgenlem  23438  1stckgen  23439  ptbasin  23462  ptbasfi  23466  dfac14lem  23502  dfac14  23503  ptuncnv  23692  ptunhmeo  23693  ptcmpfi  23698  fbun  23725  filconn  23768  isufil2  23793  ufprim  23794  fin1aufil  23817  flimclslem  23869  flimfnfcls  23913  tmdgsum  23980  tsmsgsum  24024  tsmssplit  24037  tsmsxplem1  24038  trust  24115  prdsdsf  24253  prdsmet  24256  prdsbl  24377  cnmpopc  24820  rrxmetlem  25305  rrxmet  25306  rrxdstprj1  25307  ovolctb2  25391  ovolfiniun  25400  finiunmbl  25443  volfiniun  25446  uniioombllem3  25484  uniioombllem4  25485  mbfres2  25544  itg2splitlem  25647  itg2split  25648  itgsplit  25735  limcvallem  25770  ellimc2  25776  limccnp  25790  limccnp2  25791  limcco  25792  dvmptfsum  25877  lhop2  25918  lhop  25919  mdegcl  25972  elply2  26099  elplyd  26105  ply1term  26107  ply0  26111  plyaddlem1  26116  plymullem1  26117  plymullem  26119  mtest  26311  xrlimcnp  26876  jensen  26897  fsumharmonic  26920  chtdif  27066  lgsdir2lem3  27236  lgsquadlem2  27290  dchrisumlem2  27399  dchrisum0lem1b  27424  dchrisum0lem1  27425  pntrlog2bndlem6  27492  pntlemf  27514  nosupinfsep  27642  noetasuplem4  27646  noetalem1  27651  cofcutrtime  27840  addsuniflem  27913  addsbday  27929  negsval  27936  mulsproplem12  28035  mulsproplem13  28036  mulsproplem14  28037  mulsuniflem  28057  mulsass  28074  precsexlem10  28123  bdayn0p1  28263  shsleji  31314  shsval2i  31331  ssjo  31391  sshhococi  31490  symgcom  33025  elrgspnsubrunlem1  33187  elrgspnsubrunlem2  33188  elrspunsn  33366  idlsrgtset  33445  rtelextdg2  33694  constrextdg2lem  33715  esumsplit  34020  measun  34178  aean  34211  sxbrsigalem2  34254  bnj970  34914  bnj1137  34962  subfacp1lem2a  35157  subfacp1lem3  35159  subfacp1lem5  35161  erdszelem8  35175  kur14lem7  35189  cvmliftlem10  35271  mrsubvr  35488  refssfne  36336  topjoin  36343  tailf  36353  bj-unrab  36904  bj-2upln1upl  37002  bj-ccinftyssccbar  37196  imadifss  37579  finixpnum  37589  matunitlindflem1  37600  mblfinlem4  37644  prdsbnd  37777  heibor1lem  37793  sspadd2  39799  pclfinN  39883  dochdmj1  41373  mzpcompact2lem  42728  eldioph2  42739  eldioph4b  42788  ttac  43013  pwssplit4  43066  isnumbasgrplem2  43081  isnumbasabl  43083  dfacbasgrp  43085  algsca  43154  algvsca  43155  fiuneneq  43169  tfsconcatrnss12  43326  rclexi  43592  rtrclex  43594  trclubgNEW  43595  trclexi  43597  rtrclexi  43598  cnvrcl0  43602  cnvtrcl0  43603  dfrtrcl5  43606  trrelsuperrel2dg  43648  dfrcl2  43651  relexp0a  43693  relexpaddss  43695  trclimalb2  43703  frege109d  43734  frege131d  43741  isotone1  44025  grumnudlem  44262  rnwf  44944  iblsplit  45951  fourierdlem46  46137  sge0resplit  46391  sge0split  46394  sge0splitmpt  46396  sge0xaddlem1  46418  sbgoldbo  47775  dfnbgrss  47840  gsumsplit2f  48168  setrec1  49680  elpglem2  49701