Theorem ssun2 4128

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 4127	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4107	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3979	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3896   ⊆ wss 3898

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-un 3903  df-ss 3915

This theorem is referenced by:  ssun4  4130  elun2  4132  nsspssun  4217  unv  4348  un00  4394  pwunss  4569  snsspr2  4768  snsstp3  4771  fvrn0  6859  riotassuni  7352  ovima0  7534  unexb  7689  unexbOLD  7690  difex2  7702  rnexg  7841  xpord2indlem  8086  xpord3inddlem  8093  fnsuppres  8130  brtpos0  8172  frrlem14  8238  oaabs2  8573  domunsncan  9001  mapunen  9070  ac6sfi  9179  unfir  9203  domunfican  9217  iunfi  9238  elfiun  9325  dffi3  9326  hartogslem1  9439  unwdomg  9481  unxpwdom2  9485  unxpwdom  9486  trcl  9629  unwf  9714  rankunb  9754  r0weon  9914  infxpenlem  9915  alephfplem4  10009  dju1dif  10075  cdainflem  10090  infdju  10109  cfsuc  10159  fin1a2lem10  10311  axdc3lem4  10355  ttukeylem7  10417  fpwwe2lem12  10544  canthp1lem2  10555  gchac  10583  wunrn  10631  wunex2  10640  inar1  10677  pnfxr  11177  ltrelxr  11184  un0mulcl  12426  fzdifsuc  13491  seqexw  13931  hashbclem  14366  hashf1lem1  14369  ccatrn  14504  trclublem  14909  relexprng  14960  fsumsplit  15655  o1fsum  15727  incexclem  15750  fprodsplit  15880  vdwlem5  16904  vdwlem8  16907  ramcl2  16935  srnginvl  17224  lmodvsca  17240  ipssca  17251  ipsvsca  17252  ipsip  17253  phlvsca  17261  phlip  17262  odrngtset  17318  odrngle  17319  odrngds  17320  prdssca  17367  prdsvsca  17371  prdsip  17372  prdsle  17373  prdsds  17375  prdstset  17377  prdshom  17378  prdsco  17379  imasds  17425  imassca  17431  imasvsca  17432  imasip  17433  imastset  17434  imasle  17435  mreexexlemd  17558  mreexexlem2d  17559  mreexexlem3d  17560  drsdirfi  18219  ipolerval  18446  psdmrn  18487  dirge  18517  grpinvfval  18899  mulgfval  18990  gsumzsplit  19847  gsumsplit2  19849  gsumzunsnd  19876  gsum2dlem2  19891  dprdfadd  19942  dmdprdsplit2lem  19967  dmdprdsplit2  19968  dmdprdsplit  19969  dprdsplit  19970  ablfac1eulem  19994  pgpfaclem1  20003  gsumle  20065  lspun  20929  lbsextlem2  21105  lbsextlem3  21106  lbsextlem4  21107  cnfldcj  21309  cnfldtset  21310  cnfldle  21311  cnfldds  21312  cnfldunif  21313  cnfldcjOLD  21322  cnfldtsetOLD  21323  cnfldleOLD  21324  cnflddsOLD  21325  cnfldunifOLD  21326  psrsca  21894  psrvscafval  21895  mplsubglem  21945  mplcoe5  21986  opsrtoslem2  22002  ordtbas2  23126  ordtbas  23127  ordtopn1  23129  ordtopn2  23130  leordtval2  23147  icomnfordt  23151  iooordt  23152  perfcls  23300  uncmp  23338  fiuncmp  23339  2ndcdisj2  23392  comppfsc  23467  1stckgenlem  23488  1stckgen  23489  ptbasin  23512  ptbasfi  23516  dfac14lem  23552  dfac14  23553  ptuncnv  23742  ptunhmeo  23743  ptcmpfi  23748  fbun  23775  filconn  23818  isufil2  23843  ufprim  23844  fin1aufil  23867  flimclslem  23919  flimfnfcls  23963  tmdgsum  24030  tsmsgsum  24074  tsmssplit  24087  tsmsxplem1  24088  trust  24164  prdsdsf  24302  prdsmet  24305  prdsbl  24426  cnmpopc  24869  rrxmetlem  25354  rrxmet  25355  rrxdstprj1  25356  ovolctb2  25440  ovolfiniun  25449  finiunmbl  25492  volfiniun  25495  uniioombllem3  25533  uniioombllem4  25534  mbfres2  25593  itg2splitlem  25696  itg2split  25697  itgsplit  25784  limcvallem  25819  ellimc2  25825  limccnp  25839  limccnp2  25840  limcco  25841  dvmptfsum  25926  lhop2  25967  lhop  25968  mdegcl  26021  elply2  26148  elplyd  26154  ply1term  26156  ply0  26160  plyaddlem1  26165  plymullem1  26166  plymullem  26168  mtest  26360  xrlimcnp  26925  jensen  26946  fsumharmonic  26969  chtdif  27115  lgsdir2lem3  27285  lgsquadlem2  27339  dchrisumlem2  27448  dchrisum0lem1b  27473  dchrisum0lem1  27474  pntrlog2bndlem6  27541  pntlemf  27563  nosupinfsep  27691  noetasuplem4  27695  noetalem1  27700  cofcutrtime  27891  addsuniflem  27964  addsbday  27980  negsval  27987  mulsproplem12  28086  mulsproplem13  28087  mulsproplem14  28088  mulsuniflem  28108  mulsass  28125  precsexlem10  28174  bdayn0p1  28314  shsleji  31371  shsval2i  31388  ssjo  31448  sshhococi  31547  symgcom  33093  elrgspnsubrunlem1  33257  elrgspnsubrunlem2  33258  elrspunsn  33438  idlsrgtset  33517  vieta  33664  rtelextdg2  33812  constrextdg2lem  33833  esumsplit  34138  measun  34296  aean  34329  sxbrsigalem2  34371  bnj970  35031  bnj1137  35079  subfacp1lem2a  35296  subfacp1lem3  35298  subfacp1lem5  35300  erdszelem8  35314  kur14lem7  35328  cvmliftlem10  35410  mrsubvr  35627  refssfne  36474  topjoin  36481  tailf  36491  bj-unrab  37043  bj-2upln1upl  37141  bj-ccinftyssccbar  37335  imadifss  37708  finixpnum  37718  matunitlindflem1  37729  mblfinlem4  37773  prdsbnd  37906  heibor1lem  37922  sspadd2  39988  pclfinN  40072  dochdmj1  41562  mzpcompact2lem  42908  eldioph2  42919  eldioph4b  42968  ttac  43193  pwssplit4  43246  isnumbasgrplem2  43261  isnumbasabl  43263  dfacbasgrp  43265  algsca  43334  algvsca  43335  fiuneneq  43349  tfsconcatrnss12  43506  rclexi  43772  rtrclex  43774  trclubgNEW  43775  trclexi  43777  rtrclexi  43778  cnvrcl0  43782  cnvtrcl0  43783  dfrtrcl5  43786  trrelsuperrel2dg  43828  dfrcl2  43831  relexp0a  43873  relexpaddss  43875  trclimalb2  43883  frege109d  43914  frege131d  43921  isotone1  44205  grumnudlem  44442  rnwf  45123  iblsplit  46126  fourierdlem46  46312  sge0resplit  46566  sge0split  46569  sge0splitmpt  46571  sge0xaddlem1  46593  sbgoldbo  47949  dfnbgrss  48014  gsumsplit2f  48342  setrec1  49852  elpglem2  49873