Theorem ssun2 4108

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 4107	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4088	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3958	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3886   ⊆ wss 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-or 845  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-un 3893  df-in 3895  df-ss 3905

This theorem is referenced by:  ssun4  4110  elun2  4112  nsspssun  4192  unv  4330  un00  4377  pwunss  4554  snsspr2  4749  snsstp3  4752  fvrn0  6811  riotassuni  7282  ovima0  7460  unexb  7607  difex2  7619  rnexg  7760  fnsuppres  8016  brtpos0  8058  frrlem14  8124  wfrlem16OLD  8164  oaabs2  8488  domunsncan  8868  mapunen  8942  ac6sfi  9067  unfir  9091  domunfican  9096  iunfi  9116  elfiun  9198  dffi3  9199  hartogslem1  9310  unwdomg  9352  unxpwdom2  9356  unxpwdom  9357  trcl  9495  unwf  9577  rankunb  9617  r0weon  9777  infxpenlem  9778  alephfplem4  9872  dju1dif  9937  cdainflem  9952  infdju  9973  cfsuc  10022  fin1a2lem10  10174  axdc3lem4  10218  ttukeylem7  10280  fpwwe2lem12  10407  canthp1lem2  10418  gchac  10446  wunrn  10494  wunex2  10503  inar1  10540  pnfxr  11038  ltrelxr  11045  un0mulcl  12276  fzdifsuc  13325  seqexw  13746  hashbclem  14173  hashf1lem1  14177  hashf1lem1OLD  14178  ccatrn  14303  trclublem  14715  relexprng  14766  fsumsplit  15462  o1fsum  15534  incexclem  15557  fprodsplit  15685  vdwlem5  16695  vdwlem8  16698  ramcl2  16726  srnginvl  17032  lmodvsca  17048  ipssca  17059  ipsvsca  17060  ipsip  17061  phlvsca  17069  phlip  17070  odrngtset  17126  odrngle  17127  odrngds  17128  prdssca  17176  prdsvsca  17180  prdsip  17181  prdsle  17182  prdsds  17184  prdstset  17186  prdshom  17187  prdsco  17188  imasds  17233  imassca  17239  imasvsca  17240  imasip  17241  imastset  17242  imasle  17243  mreexexlemd  17362  mreexexlem2d  17363  mreexexlem3d  17364  drsdirfi  18032  ipolerval  18259  psdmrn  18300  dirge  18330  grpinvfval  18627  mulgfval  18711  gsumzsplit  19537  gsumsplit2  19539  gsumzunsnd  19566  gsum2dlem2  19581  dprdfadd  19632  dmdprdsplit2lem  19657  dmdprdsplit2  19658  dmdprdsplit  19659  dprdsplit  19660  ablfac1eulem  19684  pgpfaclem1  19693  lspun  20258  lbsextlem2  20430  lbsextlem3  20431  lbsextlem4  20432  cnfldcj  20613  cnfldtset  20614  cnfldle  20615  cnfldds  20616  cnfldunif  20617  psrbagaddclOLD  21141  psrsca  21167  psrvscafval  21168  mplsubglem  21214  mplcoe5  21250  opsrtoslem2  21272  ordtbas2  22351  ordtbas  22352  ordtopn1  22354  ordtopn2  22355  leordtval2  22372  icomnfordt  22376  iooordt  22377  perfcls  22525  uncmp  22563  fiuncmp  22564  2ndcdisj2  22617  comppfsc  22692  1stckgenlem  22713  1stckgen  22714  ptbasin  22737  ptbasfi  22741  dfac14lem  22777  dfac14  22778  ptuncnv  22967  ptunhmeo  22968  ptcmpfi  22973  fbun  23000  filconn  23043  isufil2  23068  ufprim  23069  fin1aufil  23092  flimclslem  23144  flimfnfcls  23188  tmdgsum  23255  tsmsgsum  23299  tsmssplit  23312  tsmsxplem1  23313  trust  23390  prdsdsf  23529  prdsmet  23532  prdsbl  23656  cnmpopc  24100  rrxmetlem  24580  rrxmet  24581  rrxdstprj1  24582  ovolctb2  24665  ovolfiniun  24674  finiunmbl  24717  volfiniun  24720  uniioombllem3  24758  uniioombllem4  24759  mbfres2  24818  itg2splitlem  24922  itg2split  24923  itgsplit  25009  limcvallem  25044  ellimc2  25050  limccnp  25064  limccnp2  25065  limcco  25066  dvmptfsum  25148  lhop2  25188  lhop  25189  mdegcl  25243  elply2  25366  elplyd  25372  ply1term  25374  ply0  25378  plyaddlem1  25383  plymullem1  25384  plymullem  25386  mtest  25572  xrlimcnp  26127  jensen  26147  fsumharmonic  26170  chtdif  26316  lgsdir2lem3  26484  lgsquadlem2  26538  dchrisumlem2  26647  dchrisum0lem1b  26672  dchrisum0lem1  26673  pntrlog2bndlem6  26740  pntlemf  26762  shsleji  29741  shsval2i  29758  ssjo  29818  sshhococi  29917  gsumle  31359  symgcom  31361  idlsrgtset  31662  esumsplit  32030  measun  32188  aean  32221  sxbrsigalem2  32262  bnj970  32936  bnj1137  32984  subfacp1lem2a  33151  subfacp1lem3  33153  subfacp1lem5  33155  erdszelem8  33169  kur14lem7  33183  cvmliftlem10  33265  mrsubvr  33482  xpord2ind  33803  xpord3ind  33809  nosupinfsep  33944  noetasuplem4  33948  noetalem1  33953  cofcutrtime  34102  negsval  34132  refssfne  34556  topjoin  34563  tailf  34573  bj-unrab  35123  bj-2upln1upl  35223  bj-ccinftyssccbar  35398  imadifss  35761  finixpnum  35771  matunitlindflem1  35782  mblfinlem4  35826  prdsbnd  35960  heibor1lem  35976  sspadd2  37837  pclfinN  37921  dochdmj1  39411  mzpcompact2lem  40580  eldioph2  40591  eldioph4b  40640  ttac  40865  pwssplit4  40921  isnumbasgrplem2  40936  isnumbasabl  40938  dfacbasgrp  40940  algsca  41013  algvsca  41014  fiuneneq  41029  rclexi  41230  rtrclex  41232  trclubgNEW  41233  trclexi  41235  rtrclexi  41236  cnvrcl0  41240  cnvtrcl0  41241  dfrtrcl5  41244  trrelsuperrel2dg  41286  dfrcl2  41289  relexp0a  41331  relexpaddss  41333  trclimalb2  41341  frege109d  41372  frege131d  41379  isotone1  41665  grumnudlem  41910  iblsplit  43514  fourierdlem46  43700  sge0resplit  43951  sge0split  43954  sge0splitmpt  43956  sge0xaddlem1  43978  sbgoldbo  45250  gsumsplit2f  45385  setrec1  46408  elpglem2  46428