Theorem ssun2 4180

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 4179	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4160	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3961	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

This proof depends on syntax axioms:   ⊆ wss 3900   ∪ cun 4152

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 1945  ax-6 2002  ax-7 2043  ax-8 2149  ax-9 2157  ax-ext 2735

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2102  df-clab 2742  df-cleq 2755  df-clel 2839  df-v 3456  df-ss 3901  df-un 4154

This theorem is used by:  ssun4  4182  elun2  4184  nsspssun  4216  unv  4352  un00  4360  pwunss  4579  snsspr2  4776  snsstp3  4779  imadifssranOLD  6221  fununfun  6616  fvrn0  6944  riotassuni  7448  ovima0  7632  unexb  7795  difex2  7806  rnexg  7948  xpord2indlem  8201  xpord3inddlem  8208  fnsuppres  8246  brtpos0  8288  frrlem14  8355  oaabs2  8696  domunsncan  9134  mapunen  9203  ac6sfi  9313  unfir  9338  domunfican  9351  iunfi  9370  elfiun  9459  dffi3  9460  hartogslem1  9573  unwdomg  9615  unxpwdom2  9619  unxpwdom  9620  trcl  9766  unwf  9855  rankunb  9901  setrec1  10009  r0weon  10130  infxpenlem  10131  alephfplem4  10225  dju1dif  10290  cdainflem  10305  infdju  10324  cfsuc  10374  fin1a2lem10  10526  axdc3lem4  10570  ttukeylem7  10632  fpwwe2lem12  10766  canthp1lem2  10777  gchac  10805  wunrn  10853  wunex2  10862  inar1  10899  pnfxr  11402  ltrelxr  11409  un0mulcl  12680  fzdifsuc  13758  seqexw  14200  hashbclem  14638  hashf1lem1  14641  ccatrn  14776  trclublem  15191  relexprng  15242  fsumsplit  15951  o1fsum  16024  incexclem  16049  fprodsplit  16177  vdwlem5  17207  vdwlem8  17210  ramcl2  17238  srnginvl  17530  lmodvsca  17546  ipssca  17557  ipsvsca  17558  ipsip  17559  phlvsca  17567  phlip  17568  odrngtset  17624  odrngle  17625  odrngds  17626  prdssca  17677  prdsvsca  17681  prdsip  17682  prdsle  17683  prdsds  17685  prdstset  17687  prdshom  17688  prdsco  17689  imasds  17735  imassca  17741  imasvsca  17742  imasip  17743  imastset  17744  imasle  17745  mreexexlemd  17868  mreexexlem2d  17869  mreexexlem3d  17870  drsdirfi  18529  ipolerval  18756  psdmrn  18797  dirge  18827  grpinvfval  19239  mulgfval  19329  gsumzsplit  20192  gsumsplit2  20194  gsumzunsnd  20221  gsum2dlem2  20236  dprdfadd  20287  dmdprdsplit2lem  20312  dmdprdsplit2  20313  dmdprdsplit  20314  dprdsplit  20315  ablfac1eulem  20339  pgpfaclem1  20348  gsumle  20410  lspun  21313  lbsextlem2  21488  lbsextlem3  21489  lbsextlem4  21490  cnfldcj  21738  cnfldtset  21739  cnfldle  21740  cnfldds  21741  cnfldunif  21742  cnfldeuf  21743  psrsca  22310  psrvscafval  22311  mplsubglem  22361  mplcoe5  22404  opsrtoslem2  22420  matunitlindflem1  23049  ordtbas2  23564  ordtbas  23565  ordtopn1  23567  ordtopn2  23568  leordtval2  23585  icomnfordt  23589  iooordt  23590  perfcls  23738  uncmp  23776  fiuncmp  23777  2ndcdisj2  23831  comppfsc  23906  1stckgenlem  23927  1stckgen  23928  ptbasin  23951  ptbasfi  23955  dfac14lem  23991  dfac14  23992  ptuncnv  24181  ptunhmeo  24182  ptcmpfi  24187  fbun  24214  filconn  24257  isufil2  24282  ufprim  24283  fin1aufil  24306  flimclslem  24358  flimfnfcls  24402  tmdgsum  24469  tsmsgsum  24513  tsmssplit  24526  tsmsxplem1  24527  trust  24603  prdsdsf  24741  prdsmet  24744  prdsbl  24865  cnmpopc  25304  rrxmetlem  25783  rrxmet  25784  rrxdstprj1  25785  ovolctb2  25868  ovolfiniun  25877  finiunmbl  25920  volfiniun  25923  uniioombllem3  25961  uniioombllem4  25962  mbfres2  26021  itg2splitlem  26124  itg2split  26125  itgsplit  26211  limcvallem  26246  ellimc2  26252  limccnp  26266  limccnp2  26267  limcco  26268  dvmptfsum  26350  lhop2  26390  lhop  26391  mdegcl  26442  elply2  26569  elplyd  26575  ply1term  26577  ply0  26581  plyaddlem1  26587  plymullem1  26588  plymullem  26590  mtest  26788  xrlimcnp  27353  jensen  27373  fsumharmonic  27396  chtdif  27542  lgsdir2lem3  27711  lgsquadlem2  27765  dchrisumlem2  27874  dchrisum0lem1b  27899  dchrisum0lem1  27900  pntrlog2bndlem6  27967  pntlemf  27989  nosupinfsep  28146  noetasuplem4  28150  noetalem1  28155  cofcutrtime  28370  addsuniflem  28444  addbday  28461  negsval  28468  mulsproplem12  28570  mulsproplem13  28571  mulsproplem14  28572  mulsuniflem  28592  mulsass  28609  precsexlem10  28659  bdayn0p1  28812  shsleji  32029  shsval2i  32046  ssjo  32106  sshhococi  32205  symgcom  33743  elrgspnsubrunlem1  33907  elrgspnsubrunlem2  33908  elrspunsn  34083  idlsrgtset  34144  evls1rgspncl  34248  vieta  34323  rtelextdg2  34470  constrextdg2lem  34491  esumsplit  34796  measun  34955  aean  34988  sxbrsigalem2  35029  bnj970  35688  bnj1137  35736  subfacp1lem2a  36153  subfacp1lem3  36155  subfacp1lem5  36157  erdszelem8  36171  kur14lem7  36185  cvmliftlem10  36267  mrsubvr  36484  refssfne  37361  topjoin  37368  tailf  37378  ttcuniun  37513  ttciunun  37514  bj-unrab  38054  bj-2upln1upl  38152  bj-ccinftyssccbar  38407  imadifss  38791  finixpnum  38796  mblfinlem4  38846  prdsbnd  38993  heibor1lem  39009  sspadd2  41139  pclfinN  41223  dochdmj1  42713  mzpcompact2lem  44028  eldioph2  44039  eldioph4b  44084  ttac  44309  pwssplit4  44357  isnumbasgrplem2  44371  isnumbasabl  44373  dfacbasgrp  44375  algsca  44440  algvsca  44441  fiuneneq  44455  tfsconcatrnss12  44612  rclexi  44876  rtrclex  44878  trclubgNEW  44879  trclexi  44881  rtrclexi  44882  cnvrcl0  44886  cnvtrcl0  44887  dfrtrcl5  44890  trrelsuperrel2dg  44932  dfrcl2  44935  relexp0a  44977  relexpaddss  44979  trclimalb2  44987  frege109d  45018  frege131d  45025  isotone1  45309  grumnudlem  45530  rnwf  46220  hfrn  46283  iblsplit  47249  fourierdlem46  47435  sge0resplit  47689  sge0split  47692  sge0splitmpt  47694  sge0xaddlem1  47716  wrddun  48172  chndun  48177  chnrun  48182  sbgoldbo  49158  dfnbgrss  49223  gsumsplit2f  49550  parhomssun  51078  elpglem2  51211