Theorem ssun2 4149

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 4148	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4129	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4003	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3934   ⊆ wss 3936

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-un 3941  df-in 3943  df-ss 3952

This theorem is referenced by:  ssun4  4151  elun2  4153  nsspssun  4234  unv  4349  un00  4394  pwunss  4559  snsspr2  4748  snsstp3  4751  fvrn0  6698  riotassuni  7154  ovima0  7327  unexb  7471  difex2  7482  rnexg  7614  fnsuppres  7857  brtpos0  7899  wfrlem16  7970  oaabs2  8272  domunsncan  8617  mapunen  8686  ac6sfi  8762  unfir  8786  domunfican  8791  iunfi  8812  elfiun  8894  dffi3  8895  hartogslem1  9006  unwdomg  9048  unxpwdom2  9052  unxpwdom  9053  trcl  9170  unwf  9239  rankunb  9279  r0weon  9438  infxpenlem  9439  alephfplem4  9533  dju1dif  9598  cdainflem  9613  infdju  9630  cfsuc  9679  fin1a2lem10  9831  axdc3lem4  9875  ttukeylem7  9937  fpwwe2lem13  10064  canthp1lem2  10075  gchac  10103  wunrn  10151  wunex2  10160  inar1  10197  pnfxr  10695  ltrelxr  10702  un0mulcl  11932  fzdifsuc  12968  seqexw  13386  hashbclem  13811  hashf1lem1  13814  ccatrn  13943  trclublem  14355  relexprng  14405  fsumsplit  15097  o1fsum  15168  incexclem  15191  fprodsplit  15320  vdwlem5  16321  vdwlem8  16324  ramcl2  16352  srnginvl  16631  lmodvsca  16640  ipssca  16647  ipsvsca  16648  ipsip  16649  phlvsca  16657  phlip  16658  odrngtset  16683  odrngle  16684  odrngds  16685  prdssca  16729  prdsvsca  16733  prdsip  16734  prdsle  16735  prdsds  16737  prdstset  16739  prdshom  16740  prdsco  16741  imasds  16786  imassca  16792  imasvsca  16793  imasip  16794  imastset  16795  imasle  16796  mreexexlemd  16915  mreexexlem2d  16916  mreexexlem3d  16917  drsdirfi  17548  ipolerval  17766  psdmrn  17817  dirge  17847  grpinvfval  18142  mulgfval  18226  gsumzsplit  19047  gsumsplit2  19049  gsumzunsnd  19076  gsum2dlem2  19091  dprdfadd  19142  dmdprdsplit2lem  19167  dmdprdsplit2  19168  dmdprdsplit  19169  dprdsplit  19170  ablfac1eulem  19194  pgpfaclem1  19203  lspun  19759  lbsextlem2  19931  lbsextlem3  19932  lbsextlem4  19933  psrbagaddcl  20150  psrsca  20169  psrvscafval  20170  mplsubglem  20214  mplcoe5  20249  opsrtoslem2  20265  cnfldcj  20552  cnfldtset  20553  cnfldle  20554  cnfldds  20555  cnfldunif  20556  ordtbas2  21799  ordtbas  21800  ordtopn1  21802  ordtopn2  21803  leordtval2  21820  icomnfordt  21824  iooordt  21825  perfcls  21973  uncmp  22011  fiuncmp  22012  2ndcdisj2  22065  comppfsc  22140  1stckgenlem  22161  1stckgen  22162  ptbasin  22185  ptbasfi  22189  dfac14lem  22225  dfac14  22226  ptuncnv  22415  ptunhmeo  22416  ptcmpfi  22421  fbun  22448  filconn  22491  isufil2  22516  ufprim  22517  fin1aufil  22540  flimclslem  22592  flimfnfcls  22636  tmdgsum  22703  tsmsgsum  22747  tsmssplit  22760  tsmsxplem1  22761  trust  22838  prdsdsf  22977  prdsmet  22980  prdsbl  23101  cnmpopc  23532  rrxmetlem  24010  rrxmet  24011  rrxdstprj1  24012  ovolctb2  24093  ovolfiniun  24102  finiunmbl  24145  volfiniun  24148  uniioombllem3  24186  uniioombllem4  24187  mbfres2  24246  itg2splitlem  24349  itg2split  24350  itgsplit  24436  limcvallem  24469  ellimc2  24475  limccnp  24489  limccnp2  24490  limcco  24491  dvmptfsum  24572  lhop2  24612  lhop  24613  mdegcl  24663  elply2  24786  elplyd  24792  ply1term  24794  ply0  24798  plyaddlem1  24803  plymullem1  24804  plymullem  24806  mtest  24992  xrlimcnp  25546  jensen  25566  fsumharmonic  25589  chtdif  25735  lgsdir2lem3  25903  lgsquadlem2  25957  dchrisumlem2  26066  dchrisum0lem1b  26091  dchrisum0lem1  26092  pntrlog2bndlem6  26159  pntlemf  26181  shsleji  29147  shsval2i  29164  ssjo  29224  sshhococi  29323  gsumle  30725  symgcom  30727  esumsplit  31312  measun  31470  aean  31503  sxbrsigalem2  31544  bnj970  32219  bnj1137  32267  subfacp1lem2a  32427  subfacp1lem3  32429  subfacp1lem5  32431  erdszelem8  32445  kur14lem7  32459  cvmliftlem10  32541  mrsubvr  32758  frrlem14  33136  noetalem3  33219  refssfne  33706  topjoin  33713  tailf  33723  bj-unrab  34247  bj-2upln1upl  34339  bj-ccinftyssccbar  34503  imadifss  34882  finixpnum  34892  matunitlindflem1  34903  mblfinlem4  34947  prdsbnd  35086  heibor1lem  35102  sspadd2  36967  pclfinN  37051  dochdmj1  38541  mzpcompact2lem  39368  eldioph2  39379  eldioph4b  39428  ttac  39653  pwssplit4  39709  isnumbasgrplem2  39724  isnumbasabl  39726  dfacbasgrp  39728  algsca  39801  algvsca  39802  fiuneneq  39817  rclexi  39995  rtrclex  39997  trclubgNEW  39998  trclexi  40000  rtrclexi  40001  cnvrcl0  40005  cnvtrcl0  40006  dfrtrcl5  40009  trrelsuperrel2dg  40036  dfrcl2  40039  relexp0a  40081  relexpaddss  40083  trclimalb2  40091  frege109d  40122  frege131d  40129  isotone1  40418  grumnudlem  40641  iblsplit  42271  fourierdlem46  42457  sge0resplit  42708  sge0split  42711  sge0splitmpt  42713  sge0xaddlem1  42735  sbgoldbo  43972  gsumsplit2f  44107  setrec1  44814  elpglem2  44834