Theorem ssun2 4176

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 4175	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4156	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3957	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

This proof depends on syntax axioms:   ⊆ wss 3896   ∪ cun 4148

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-ss 3897  df-un 4150

This theorem is used by:  ssun4  4178  elun2  4180  nsspssun  4212  unv  4348  un00  4356  pwunss  4575  snsspr2  4770  snsstp3  4773  imadifssranOLD  6204  fvrn0  6916  riotassuni  7419  ovima0  7602  unexb  7765  difex2  7776  rnexg  7916  xpord2indlem  8168  xpord3inddlem  8175  fnsuppres  8213  brtpos0  8255  frrlem14  8322  oaabs2  8663  domunsncan  9101  mapunen  9170  ac6sfi  9280  unfir  9305  domunfican  9318  iunfi  9337  elfiun  9427  dffi3  9428  hartogslem1  9541  unwdomg  9583  unxpwdom2  9587  unxpwdom  9588  trcl  9734  unwf  9823  rankunb  9869  setrec1  9977  r0weon  10096  infxpenlem  10097  alephfplem4  10191  dju1dif  10256  cdainflem  10271  infdju  10290  cfsuc  10340  fin1a2lem10  10492  axdc3lem4  10536  ttukeylem7  10598  fpwwe2lem12  10732  canthp1lem2  10743  gchac  10771  wunrn  10819  wunex2  10828  inar1  10865  pnfxr  11368  ltrelxr  11375  un0mulcl  12645  fzdifsuc  13723  seqexw  14165  hashbclem  14602  hashf1lem1  14605  ccatrn  14740  trclublem  15155  relexprng  15206  fsumsplit  15914  o1fsum  15987  incexclem  16012  fprodsplit  16140  vdwlem5  17170  vdwlem8  17173  ramcl2  17201  srnginvl  17491  lmodvsca  17507  ipssca  17518  ipsvsca  17519  ipsip  17520  phlvsca  17528  phlip  17529  odrngtset  17585  odrngle  17586  odrngds  17587  prdssca  17634  prdsvsca  17638  prdsip  17639  prdsle  17640  prdsds  17642  prdstset  17644  prdshom  17645  prdsco  17646  imasds  17692  imassca  17698  imasvsca  17699  imasip  17700  imastset  17701  imasle  17702  mreexexlemd  17825  mreexexlem2d  17826  mreexexlem3d  17827  drsdirfi  18486  ipolerval  18713  psdmrn  18754  dirge  18784  grpinvfval  19196  mulgfval  19286  gsumzsplit  20148  gsumsplit2  20150  gsumzunsnd  20177  gsum2dlem2  20192  dprdfadd  20243  dmdprdsplit2lem  20268  dmdprdsplit2  20269  dmdprdsplit  20270  dprdsplit  20271  ablfac1eulem  20295  pgpfaclem1  20304  gsumle  20366  lspun  21269  lbsextlem2  21444  lbsextlem3  21445  lbsextlem4  21446  cnfldcj  21694  cnfldtset  21695  cnfldle  21696  cnfldds  21697  cnfldunif  21698  psrsca  22262  psrvscafval  22263  mplsubglem  22313  mplcoe5  22356  opsrtoslem2  22372  matunitlindflem1  23001  ordtbas2  23516  ordtbas  23517  ordtopn1  23519  ordtopn2  23520  leordtval2  23537  icomnfordt  23541  iooordt  23542  perfcls  23690  uncmp  23728  fiuncmp  23729  2ndcdisj2  23783  comppfsc  23858  1stckgenlem  23879  1stckgen  23880  ptbasin  23903  ptbasfi  23907  dfac14lem  23943  dfac14  23944  ptuncnv  24133  ptunhmeo  24134  ptcmpfi  24139  fbun  24166  filconn  24209  isufil2  24234  ufprim  24235  fin1aufil  24258  flimclslem  24310  flimfnfcls  24354  tmdgsum  24421  tsmsgsum  24465  tsmssplit  24478  tsmsxplem1  24479  trust  24555  prdsdsf  24693  prdsmet  24696  prdsbl  24817  cnmpopc  25256  rrxmetlem  25735  rrxmet  25736  rrxdstprj1  25737  ovolctb2  25820  ovolfiniun  25829  finiunmbl  25872  volfiniun  25875  uniioombllem3  25913  uniioombllem4  25914  mbfres2  25973  itg2splitlem  26076  itg2split  26077  itgsplit  26163  limcvallem  26198  ellimc2  26204  limccnp  26218  limccnp2  26219  limcco  26220  dvmptfsum  26302  lhop2  26342  lhop  26343  mdegcl  26394  elply2  26521  elplyd  26527  ply1term  26529  ply0  26533  plyaddlem1  26539  plymullem1  26540  plymullem  26542  mtest  26738  xrlimcnp  27303  jensen  27323  fsumharmonic  27346  chtdif  27492  lgsdir2lem3  27661  lgsquadlem2  27715  dchrisumlem2  27824  dchrisum0lem1b  27849  dchrisum0lem1  27850  pntrlog2bndlem6  27917  pntlemf  27939  nosupinfsep  28096  noetasuplem4  28100  noetalem1  28105  cofcutrtime  28320  addsuniflem  28394  addbday  28411  negsval  28418  mulsproplem12  28520  mulsproplem13  28521  mulsproplem14  28522  mulsuniflem  28542  mulsass  28559  precsexlem10  28609  bdayn0p1  28762  shsleji  31979  shsval2i  31996  ssjo  32056  sshhococi  32155  symgcom  33692  elrgspnsubrunlem1  33856  elrgspnsubrunlem2  33857  elrspunsn  34027  idlsrgtset  34088  vieta  34260  rtelextdg2  34407  constrextdg2lem  34428  esumsplit  34733  measun  34892  aean  34925  sxbrsigalem2  34966  bnj970  35625  bnj1137  35673  subfacp1lem2a  36033  subfacp1lem3  36035  subfacp1lem5  36037  erdszelem8  36051  kur14lem7  36065  cvmliftlem10  36147  mrsubvr  36364  refssfne  37240  topjoin  37247  tailf  37257  ttcuniun  37392  ttciunun  37393  bj-unrab  37933  bj-2upln1upl  38031  bj-ccinftyssccbar  38246  imadifss  38630  finixpnum  38635  mblfinlem4  38685  prdsbnd  38834  heibor1lem  38850  sspadd2  40980  pclfinN  41064  dochdmj1  42554  mzpcompact2lem  43869  eldioph2  43880  eldioph4b  43925  ttac  44150  pwssplit4  44198  isnumbasgrplem2  44213  isnumbasabl  44215  dfacbasgrp  44217  algsca  44286  algvsca  44287  fiuneneq  44301  tfsconcatrnss12  44458  rclexi  44722  rtrclex  44724  trclubgNEW  44725  trclexi  44727  rtrclexi  44728  cnvrcl0  44732  cnvtrcl0  44733  dfrtrcl5  44736  trrelsuperrel2dg  44778  dfrcl2  44781  relexp0a  44823  relexpaddss  44825  trclimalb2  44833  frege109d  44864  frege131d  44871  isotone1  45155  grumnudlem  45376  rnwf  46063  hfrn  46126  iblsplit  47083  fourierdlem46  47269  sge0resplit  47523  sge0split  47526  sge0splitmpt  47528  sge0xaddlem1  47550  wrddun  48006  chndun  48011  chnrun  48016  sbgoldbo  48992  dfnbgrss  49057  gsumsplit2f  49384  parhomssun  50854  elpglem2  50987