Theorem ssun2 3739

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 3738	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 3719	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3600	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3538   ⊆ wss 3540

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590

This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-un 3545  df-in 3547  df-ss 3554

This theorem is referenced by:  ssun4  3741  elun2  3743  nsspssun  3819  unv  3923  un00  3963  snsspr2  4286  snsstp3  4289  fvrn0  6126  riotassuni  6547  ovima0  6711  unexb  6856  difex2  6863  rnexg  6990  fnsuppres  7209  brtpos0  7246  wfrlem16  7317  oaabs2  7612  domunsncan  7945  mapunen  8014  ac6sfi  8089  unfir  8113  domunfican  8118  iunfi  8137  elfiun  8219  dffi3  8220  hartogslem1  8330  unwdomg  8372  unxpwdom2  8376  unxpwdom  8377  trcl  8487  unwf  8556  rankunb  8596  r0weon  8718  infxpenlem  8719  alephfplem4  8813  cda1dif  8881  cdainflem  8896  infcda  8913  cfsuc  8962  fin1a2lem10  9114  axdc3lem4  9158  ttukeylem7  9220  fpwwe2lem13  9343  canthp1lem2  9354  gchac  9382  wunrn  9430  wunex2  9439  inar1  9476  pnfxr  9971  ltrelxr  9978  un0mulcl  11204  fzdifsuc  12270  hashbclem  13093  hashf1lem1  13096  ccatrn  13225  trclublem  13582  relexprng  13634  fsumsplit  14318  o1fsum  14386  incexclem  14407  fprodsplit  14535  vdwlem5  15527  vdwlem8  15530  ramcl2  15558  srnginvl  15835  lmodvsca  15844  ipssca  15851  ipsvsca  15852  ipsip  15853  phlvsca  15861  phlip  15862  odrngtset  15893  odrngle  15894  odrngds  15895  prdssca  15939  prdsvsca  15943  prdsip  15944  prdsle  15945  prdsds  15947  prdstset  15949  prdshom  15950  prdsco  15951  imasds  15996  imassca  16002  imasvsca  16003  imasip  16004  imastset  16005  imasle  16006  mreexexlemd  16127  mreexexlem2d  16128  mreexexlem3d  16129  drsdirfi  16761  ipolerval  16979  psdmrn  17030  dirge  17060  gsumzsplit  18150  gsumsplit2  18152  gsumzunsnd  18178  gsum2dlem2  18193  dprdfadd  18242  dmdprdsplit2lem  18267  dmdprdsplit2  18268  dmdprdsplit  18269  dprdsplit  18270  ablfac1eulem  18294  pgpfaclem1  18303  lspun  18808  lbsextlem2  18980  lbsextlem3  18981  lbsextlem4  18982  psrbagaddcl  19191  psrsca  19210  psrvscafval  19211  mplsubglem  19255  mplcoe5  19289  opsrtoslem2  19306  cnfldcj  19574  cnfldtset  19575  cnfldle  19576  cnfldds  19577  cnfldunif  19578  ordtbas2  20805  ordtbas  20806  ordtopn1  20808  ordtopn2  20809  leordtval2  20826  icomnfordt  20830  iooordt  20831  perfcls  20979  uncmp  21016  fiuncmp  21017  2ndcdisj2  21070  comppfsc  21145  1stckgenlem  21166  1stckgen  21167  ptbasin  21190  ptbasfi  21194  dfac14lem  21230  dfac14  21231  ptuncnv  21420  ptunhmeo  21421  ptcmpfi  21426  fbun  21454  filcon  21497  isufil2  21522  ufprim  21523  fin1aufil  21546  flimclslem  21598  flimfnfcls  21642  tmdgsum  21709  tsmsgsum  21752  tsmssplit  21765  tsmsxplem1  21766  trust  21843  prdsdsf  21982  prdsmet  21985  prdsbl  22106  cnmpt2pc  22535  rrxmetlem  22998  rrxmet  22999  rrxdstprj1  23000  ovolctb2  23067  ovolfiniun  23076  finiunmbl  23119  volfiniun  23122  uniioombllem3  23159  uniioombllem4  23160  mbfres2  23218  itg2splitlem  23321  itg2split  23322  itgsplit  23408  limcvallem  23441  ellimc2  23447  limccnp  23461  limccnp2  23462  limcco  23463  dvmptfsum  23542  lhop2  23582  lhop  23583  mdegcl  23633  elply2  23756  elplyd  23762  ply1term  23764  ply0  23768  plyaddlem1  23773  plymullem1  23774  plymullem  23776  mtest  23962  xrlimcnp  24495  jensen  24515  fsumharmonic  24538  chtdif  24684  lgsdir2lem3  24852  lgsquadlem2  24906  dchrisumlem2  24979  dchrisum0lem1b  25004  dchrisum0lem1  25005  pntrlog2bndlem6  25072  pntlemf  25094  eupap1  26503  shsleji  27613  shsval2i  27630  ssjo  27690  sshhococi  27789  gsumle  29110  esumsplit  29442  measun  29601  aean  29634  sxbrsigalem2  29675  bnj970  30271  bnj1137  30317  subfacp1lem2a  30416  subfacp1lem3  30418  subfacp1lem5  30420  erdszelem8  30434  kur14lem7  30448  cvmliftlem10  30530  mrsubvr  30662  nofulllem4  31104  refssfne  31523  topjoin  31530  tailf  31540  bj-unrab  32114  bj-2upln1upl  32205  bj-ccinftyssccbar  32282  imadifss  32554  finixpnum  32564  matunitlindflem1  32575  mblfinlem4  32619  prdsbnd  32762  heibor1lem  32778  sspadd2  34120  pclfinN  34204  dochdmj1  35697  mzpcompact2lem  36332  eldioph2  36343  eldioph4b  36393  ttac  36621  pwssplit4  36677  isnumbasgrplem2  36693  isnumbasabl  36695  dfacbasgrp  36697  algsca  36770  algvsca  36771  fiuneneq  36794  rclexi  36941  rtrclex  36943  trclubgNEW  36944  trclexi  36946  rtrclexi  36947  cnvrcl0  36951  cnvtrcl0  36952  dfrtrcl5  36955  trrelsuperrel2dg  36982  dfrcl2  36985  relexp0a  37027  relexpaddss  37029  trclimalb2  37037  frege109d  37068  frege131d  37075  isotone1  37366  iblsplit  38858  fourierdlem46  39045  sge0resplit  39299  sge0split  39302  sge0splitmpt  39304  sge0xaddlem1  39326  gsumsplit2f  41936  setrec1  42237  elpglem2  42254