Theorem ssun2 4159

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 4158	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4138	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4012	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3929   ⊆ wss 3931

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 2708

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 2715  df-cleq 2728  df-clel 2810  df-v 3466  df-un 3936  df-ss 3948

This theorem is referenced by:  ssun4  4161  elun2  4163  nsspssun  4248  unv  4379  un00  4425  pwunss  4598  snsspr2  4796  snsstp3  4799  fvrn0  6911  riotassuni  7407  ovima0  7591  unexb  7746  unexbOLD  7747  difex2  7759  rnexg  7903  xpord2indlem  8151  xpord3inddlem  8158  fnsuppres  8195  brtpos0  8237  frrlem14  8303  wfrlem16OLD  8343  oaabs2  8666  domunsncan  9091  mapunen  9165  ac6sfi  9297  unfir  9323  domunfican  9338  iunfi  9360  elfiun  9447  dffi3  9448  hartogslem1  9561  unwdomg  9603  unxpwdom2  9607  unxpwdom  9608  trcl  9747  unwf  9829  rankunb  9869  r0weon  10031  infxpenlem  10032  alephfplem4  10126  dju1dif  10192  cdainflem  10207  infdju  10226  cfsuc  10276  fin1a2lem10  10428  axdc3lem4  10472  ttukeylem7  10534  fpwwe2lem12  10661  canthp1lem2  10672  gchac  10700  wunrn  10748  wunex2  10757  inar1  10794  pnfxr  11294  ltrelxr  11301  un0mulcl  12540  fzdifsuc  13606  seqexw  14040  hashbclem  14475  hashf1lem1  14478  ccatrn  14612  trclublem  15019  relexprng  15070  fsumsplit  15762  o1fsum  15834  incexclem  15857  fprodsplit  15987  vdwlem5  17010  vdwlem8  17013  ramcl2  17041  srnginvl  17332  lmodvsca  17348  ipssca  17359  ipsvsca  17360  ipsip  17361  phlvsca  17369  phlip  17370  odrngtset  17426  odrngle  17427  odrngds  17428  prdssca  17475  prdsvsca  17479  prdsip  17480  prdsle  17481  prdsds  17483  prdstset  17485  prdshom  17486  prdsco  17487  imasds  17532  imassca  17538  imasvsca  17539  imasip  17540  imastset  17541  imasle  17542  mreexexlemd  17661  mreexexlem2d  17662  mreexexlem3d  17663  drsdirfi  18322  ipolerval  18547  psdmrn  18588  dirge  18618  grpinvfval  18966  mulgfval  19057  gsumzsplit  19913  gsumsplit2  19915  gsumzunsnd  19942  gsum2dlem2  19957  dprdfadd  20008  dmdprdsplit2lem  20033  dmdprdsplit2  20034  dmdprdsplit  20035  dprdsplit  20036  ablfac1eulem  20060  pgpfaclem1  20069  lspun  20949  lbsextlem2  21125  lbsextlem3  21126  lbsextlem4  21127  cnfldcj  21329  cnfldtset  21330  cnfldle  21331  cnfldds  21332  cnfldunif  21333  cnfldcjOLD  21342  cnfldtsetOLD  21343  cnfldleOLD  21344  cnflddsOLD  21345  cnfldunifOLD  21346  psrsca  21912  psrvscafval  21913  mplsubglem  21964  mplcoe5  22003  opsrtoslem2  22019  ordtbas2  23134  ordtbas  23135  ordtopn1  23137  ordtopn2  23138  leordtval2  23155  icomnfordt  23159  iooordt  23160  perfcls  23308  uncmp  23346  fiuncmp  23347  2ndcdisj2  23400  comppfsc  23475  1stckgenlem  23496  1stckgen  23497  ptbasin  23520  ptbasfi  23524  dfac14lem  23560  dfac14  23561  ptuncnv  23750  ptunhmeo  23751  ptcmpfi  23756  fbun  23783  filconn  23826  isufil2  23851  ufprim  23852  fin1aufil  23875  flimclslem  23927  flimfnfcls  23971  tmdgsum  24038  tsmsgsum  24082  tsmssplit  24095  tsmsxplem1  24096  trust  24173  prdsdsf  24311  prdsmet  24314  prdsbl  24435  cnmpopc  24878  rrxmetlem  25364  rrxmet  25365  rrxdstprj1  25366  ovolctb2  25450  ovolfiniun  25459  finiunmbl  25502  volfiniun  25505  uniioombllem3  25543  uniioombllem4  25544  mbfres2  25603  itg2splitlem  25706  itg2split  25707  itgsplit  25794  limcvallem  25829  ellimc2  25835  limccnp  25849  limccnp2  25850  limcco  25851  dvmptfsum  25936  lhop2  25977  lhop  25978  mdegcl  26031  elply2  26158  elplyd  26164  ply1term  26166  ply0  26170  plyaddlem1  26175  plymullem1  26176  plymullem  26178  mtest  26370  xrlimcnp  26935  jensen  26956  fsumharmonic  26979  chtdif  27125  lgsdir2lem3  27295  lgsquadlem2  27349  dchrisumlem2  27458  dchrisum0lem1b  27483  dchrisum0lem1  27484  pntrlog2bndlem6  27551  pntlemf  27573  nosupinfsep  27701  noetasuplem4  27705  noetalem1  27710  cofcutrtime  27892  addsuniflem  27965  addsbday  27981  negsval  27988  mulsproplem12  28087  mulsproplem13  28088  mulsproplem14  28089  mulsuniflem  28109  mulsass  28126  precsexlem10  28175  bdayn0p1  28315  shsleji  31356  shsval2i  31373  ssjo  31433  sshhococi  31532  gsumle  33097  symgcom  33099  elrgspnsubrunlem1  33247  elrgspnsubrunlem2  33248  elrspunsn  33449  idlsrgtset  33528  rtelextdg2  33766  constrextdg2lem  33787  esumsplit  34089  measun  34247  aean  34280  sxbrsigalem2  34323  bnj970  34983  bnj1137  35031  subfacp1lem2a  35207  subfacp1lem3  35209  subfacp1lem5  35211  erdszelem8  35225  kur14lem7  35239  cvmliftlem10  35321  mrsubvr  35538  refssfne  36381  topjoin  36388  tailf  36398  bj-unrab  36949  bj-2upln1upl  37047  bj-ccinftyssccbar  37241  imadifss  37624  finixpnum  37634  matunitlindflem1  37645  mblfinlem4  37689  prdsbnd  37822  heibor1lem  37838  sspadd2  39840  pclfinN  39924  dochdmj1  41414  mzpcompact2lem  42749  eldioph2  42760  eldioph4b  42809  ttac  43035  pwssplit4  43088  isnumbasgrplem2  43103  isnumbasabl  43105  dfacbasgrp  43107  algsca  43176  algvsca  43177  fiuneneq  43191  tfsconcatrnss12  43348  rclexi  43614  rtrclex  43616  trclubgNEW  43617  trclexi  43619  rtrclexi  43620  cnvrcl0  43624  cnvtrcl0  43625  dfrtrcl5  43628  trrelsuperrel2dg  43670  dfrcl2  43673  relexp0a  43715  relexpaddss  43717  trclimalb2  43725  frege109d  43756  frege131d  43763  isotone1  44047  grumnudlem  44284  rnwf  44966  iblsplit  45975  fourierdlem46  46161  sge0resplit  46415  sge0split  46418  sge0splitmpt  46420  sge0xaddlem1  46442  sbgoldbo  47781  dfnbgrss  47845  gsumsplit2f  48135  setrec1  49535  elpglem2  49556