Theorem ssun2 4125

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 4124	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4105	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3979	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

This proof depends on syntax axioms:   ∪ cun 3897   ⊆ wss 3899

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-un 3904  df-ss 3916

This theorem is used by:  ssun4  4127  elun2  4129  nsspssun  4214  unv  4349  un00  4357  pwunss  4575  snsspr2  4776  snsstp3  4779  imadifssranOLD  6201  fvrn0  6911  riotassuni  7415  ovima0  7598  unexb  7761  difex2  7772  rnexg  7912  xpord2indlem  8157  xpord3inddlem  8164  fnsuppres  8201  brtpos0  8243  frrlem14  8310  oaabs2  8651  domunsncan  9089  mapunen  9158  ac6sfi  9268  unfir  9293  domunfican  9306  iunfi  9325  elfiun  9415  dffi3  9416  hartogslem1  9529  unwdomg  9571  unxpwdom2  9575  unxpwdom  9576  trcl  9722  unwf  9811  rankunb  9857  setrec1  9965  r0weon  10084  infxpenlem  10085  alephfplem4  10179  dju1dif  10244  cdainflem  10259  infdju  10278  cfsuc  10328  fin1a2lem10  10480  axdc3lem4  10524  ttukeylem7  10586  fpwwe2lem12  10720  canthp1lem2  10731  gchac  10759  wunrn  10807  wunex2  10816  inar1  10853  pnfxr  11356  ltrelxr  11363  un0mulcl  12633  fzdifsuc  13711  seqexw  14153  hashbclem  14590  hashf1lem1  14593  ccatrn  14728  trclublem  15141  relexprng  15192  fsumsplit  15900  o1fsum  15973  incexclem  15998  fprodsplit  16126  vdwlem5  17156  vdwlem8  17159  ramcl2  17187  srnginvl  17477  lmodvsca  17493  ipssca  17504  ipsvsca  17505  ipsip  17506  phlvsca  17514  phlip  17515  odrngtset  17571  odrngle  17572  odrngds  17573  prdssca  17620  prdsvsca  17624  prdsip  17625  prdsle  17626  prdsds  17628  prdstset  17630  prdshom  17631  prdsco  17632  imasds  17678  imassca  17684  imasvsca  17685  imasip  17686  imastset  17687  imasle  17688  mreexexlemd  17811  mreexexlem2d  17812  mreexexlem3d  17813  drsdirfi  18472  ipolerval  18699  psdmrn  18740  dirge  18770  grpinvfval  19182  mulgfval  19272  gsumzsplit  20134  gsumsplit2  20136  gsumzunsnd  20163  gsum2dlem2  20178  dprdfadd  20229  dmdprdsplit2lem  20254  dmdprdsplit2  20255  dmdprdsplit  20256  dprdsplit  20257  ablfac1eulem  20281  pgpfaclem1  20290  gsumle  20352  lspun  21255  lbsextlem2  21430  lbsextlem3  21431  lbsextlem4  21432  cnfldcj  21680  cnfldtset  21681  cnfldle  21682  cnfldds  21683  cnfldunif  21684  psrsca  22248  psrvscafval  22249  mplsubglem  22299  mplcoe5  22342  opsrtoslem2  22358  matunitlindflem1  22987  ordtbas2  23502  ordtbas  23503  ordtopn1  23505  ordtopn2  23506  leordtval2  23523  icomnfordt  23527  iooordt  23528  perfcls  23676  uncmp  23714  fiuncmp  23715  2ndcdisj2  23769  comppfsc  23844  1stckgenlem  23865  1stckgen  23866  ptbasin  23889  ptbasfi  23893  dfac14lem  23929  dfac14  23930  ptuncnv  24119  ptunhmeo  24120  ptcmpfi  24125  fbun  24152  filconn  24195  isufil2  24220  ufprim  24221  fin1aufil  24244  flimclslem  24296  flimfnfcls  24340  tmdgsum  24407  tsmsgsum  24451  tsmssplit  24464  tsmsxplem1  24465  trust  24541  prdsdsf  24679  prdsmet  24682  prdsbl  24803  cnmpopc  25242  rrxmetlem  25721  rrxmet  25722  rrxdstprj1  25723  ovolctb2  25806  ovolfiniun  25815  finiunmbl  25858  volfiniun  25861  uniioombllem3  25899  uniioombllem4  25900  mbfres2  25959  itg2splitlem  26062  itg2split  26063  itgsplit  26149  limcvallem  26184  ellimc2  26190  limccnp  26204  limccnp2  26205  limcco  26206  dvmptfsum  26288  lhop2  26328  lhop  26329  mdegcl  26380  elply2  26507  elplyd  26513  ply1term  26515  ply0  26519  plyaddlem1  26525  plymullem1  26526  plymullem  26528  mtest  26724  xrlimcnp  27289  jensen  27309  fsumharmonic  27332  chtdif  27478  lgsdir2lem3  27647  lgsquadlem2  27701  dchrisumlem2  27810  dchrisum0lem1b  27835  dchrisum0lem1  27836  pntrlog2bndlem6  27903  pntlemf  27925  nosupinfsep  28082  noetasuplem4  28086  noetalem1  28091  cofcutrtime  28306  addsuniflem  28380  addbday  28397  negsval  28404  mulsproplem12  28506  mulsproplem13  28507  mulsproplem14  28508  mulsuniflem  28528  mulsass  28545  precsexlem10  28595  bdayn0p1  28748  shsleji  31965  shsval2i  31982  ssjo  32042  sshhococi  32141  symgcom  33637  elrgspnsubrunlem1  33801  elrgspnsubrunlem2  33802  elrspunsn  33972  idlsrgtset  34033  vieta  34205  rtelextdg2  34352  constrextdg2lem  34373  esumsplit  34678  measun  34837  aean  34870  sxbrsigalem2  34911  bnj970  35570  bnj1137  35618  subfacp1lem2a  35924  subfacp1lem3  35926  subfacp1lem5  35928  erdszelem8  35942  kur14lem7  35956  cvmliftlem10  36038  mrsubvr  36255  refssfne  37126  topjoin  37133  tailf  37143  ttcuniun  37278  ttciunun  37279  bj-unrab  37819  bj-2upln1upl  37917  bj-ccinftyssccbar  38119  imadifss  38503  finixpnum  38508  mblfinlem4  38558  prdsbnd  38707  heibor1lem  38723  sspadd2  40853  pclfinN  40937  dochdmj1  42427  mzpcompact2lem  43741  eldioph2  43752  eldioph4b  43797  ttac  44022  pwssplit4  44075  isnumbasgrplem2  44090  isnumbasabl  44092  dfacbasgrp  44094  algsca  44163  algvsca  44164  fiuneneq  44178  tfsconcatrnss12  44335  rclexi  44600  rtrclex  44602  trclubgNEW  44603  trclexi  44605  rtrclexi  44606  cnvrcl0  44610  cnvtrcl0  44611  dfrtrcl5  44614  trrelsuperrel2dg  44656  dfrcl2  44659  relexp0a  44701  relexpaddss  44703  trclimalb2  44711  frege109d  44742  frege131d  44749  isotone1  45033  grumnudlem  45254  rnwf  45934  hfrn  45997  iblsplit  46945  fourierdlem46  47131  sge0resplit  47385  sge0split  47388  sge0splitmpt  47390  sge0xaddlem1  47412  wrddun  47868  chndun  47873  chnrun  47878  sbgoldbo  48854  dfnbgrss  48919  gsumsplit2f  49246  elpglem2  50774