Theorem ssun2 4202

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 4201	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4181	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4045	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3974   ⊆ wss 3976

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-un 3981  df-ss 3993

This theorem is referenced by:  ssun4  4204  elun2  4206  nsspssun  4287  unv  4422  un00  4468  pwunss  4640  snsspr2  4840  snsstp3  4843  fvrn0  6950  riotassuni  7445  ovima0  7629  unexb  7782  unexbOLD  7783  difex2  7795  rnexg  7942  xpord2indlem  8188  xpord3inddlem  8195  fnsuppres  8232  brtpos0  8274  frrlem14  8340  wfrlem16OLD  8380  oaabs2  8705  domunsncan  9138  mapunen  9212  ac6sfi  9348  unfir  9374  domunfican  9389  iunfi  9411  elfiun  9499  dffi3  9500  hartogslem1  9611  unwdomg  9653  unxpwdom2  9657  unxpwdom  9658  trcl  9797  unwf  9879  rankunb  9919  r0weon  10081  infxpenlem  10082  alephfplem4  10176  dju1dif  10242  cdainflem  10257  infdju  10276  cfsuc  10326  fin1a2lem10  10478  axdc3lem4  10522  ttukeylem7  10584  fpwwe2lem12  10711  canthp1lem2  10722  gchac  10750  wunrn  10798  wunex2  10807  inar1  10844  pnfxr  11344  ltrelxr  11351  un0mulcl  12587  fzdifsuc  13644  seqexw  14068  hashbclem  14501  hashf1lem1  14504  ccatrn  14637  trclublem  15044  relexprng  15095  fsumsplit  15789  o1fsum  15861  incexclem  15884  fprodsplit  16014  vdwlem5  17032  vdwlem8  17035  ramcl2  17063  srnginvl  17372  lmodvsca  17388  ipssca  17399  ipsvsca  17400  ipsip  17401  phlvsca  17409  phlip  17410  odrngtset  17466  odrngle  17467  odrngds  17468  prdssca  17516  prdsvsca  17520  prdsip  17521  prdsle  17522  prdsds  17524  prdstset  17526  prdshom  17527  prdsco  17528  imasds  17573  imassca  17579  imasvsca  17580  imasip  17581  imastset  17582  imasle  17583  mreexexlemd  17702  mreexexlem2d  17703  mreexexlem3d  17704  drsdirfi  18375  ipolerval  18602  psdmrn  18643  dirge  18673  grpinvfval  19018  mulgfval  19109  gsumzsplit  19969  gsumsplit2  19971  gsumzunsnd  19998  gsum2dlem2  20013  dprdfadd  20064  dmdprdsplit2lem  20089  dmdprdsplit2  20090  dmdprdsplit  20091  dprdsplit  20092  ablfac1eulem  20116  pgpfaclem1  20125  lspun  21008  lbsextlem2  21184  lbsextlem3  21185  lbsextlem4  21186  cnfldcj  21396  cnfldtset  21397  cnfldle  21398  cnfldds  21399  cnfldunif  21400  cnfldcjOLD  21409  cnfldtsetOLD  21410  cnfldleOLD  21411  cnflddsOLD  21412  cnfldunifOLD  21413  psrsca  21990  psrvscafval  21991  mplsubglem  22042  mplcoe5  22081  opsrtoslem2  22103  ordtbas2  23220  ordtbas  23221  ordtopn1  23223  ordtopn2  23224  leordtval2  23241  icomnfordt  23245  iooordt  23246  perfcls  23394  uncmp  23432  fiuncmp  23433  2ndcdisj2  23486  comppfsc  23561  1stckgenlem  23582  1stckgen  23583  ptbasin  23606  ptbasfi  23610  dfac14lem  23646  dfac14  23647  ptuncnv  23836  ptunhmeo  23837  ptcmpfi  23842  fbun  23869  filconn  23912  isufil2  23937  ufprim  23938  fin1aufil  23961  flimclslem  24013  flimfnfcls  24057  tmdgsum  24124  tsmsgsum  24168  tsmssplit  24181  tsmsxplem1  24182  trust  24259  prdsdsf  24398  prdsmet  24401  prdsbl  24525  cnmpopc  24974  rrxmetlem  25460  rrxmet  25461  rrxdstprj1  25462  ovolctb2  25546  ovolfiniun  25555  finiunmbl  25598  volfiniun  25601  uniioombllem3  25639  uniioombllem4  25640  mbfres2  25699  itg2splitlem  25803  itg2split  25804  itgsplit  25891  limcvallem  25926  ellimc2  25932  limccnp  25946  limccnp2  25947  limcco  25948  dvmptfsum  26033  lhop2  26074  lhop  26075  mdegcl  26128  elply2  26255  elplyd  26261  ply1term  26263  ply0  26267  plyaddlem1  26272  plymullem1  26273  plymullem  26275  mtest  26465  xrlimcnp  27029  jensen  27050  fsumharmonic  27073  chtdif  27219  lgsdir2lem3  27389  lgsquadlem2  27443  dchrisumlem2  27552  dchrisum0lem1b  27577  dchrisum0lem1  27578  pntrlog2bndlem6  27645  pntlemf  27667  nosupinfsep  27795  noetasuplem4  27799  noetalem1  27804  cofcutrtime  27979  addsuniflem  28052  addsbday  28068  negsval  28075  mulsproplem12  28171  mulsproplem13  28172  mulsproplem14  28173  mulsuniflem  28193  mulsass  28210  precsexlem10  28258  shsleji  31402  shsval2i  31419  ssjo  31479  sshhococi  31578  gsumle  33074  symgcom  33076  elrspunsn  33422  idlsrgtset  33501  rtelextdg2  33718  esumsplit  34017  measun  34175  aean  34208  sxbrsigalem2  34251  bnj970  34923  bnj1137  34971  subfacp1lem2a  35148  subfacp1lem3  35150  subfacp1lem5  35152  erdszelem8  35166  kur14lem7  35180  cvmliftlem10  35262  mrsubvr  35479  refssfne  36324  topjoin  36331  tailf  36341  bj-unrab  36892  bj-2upln1upl  36990  bj-ccinftyssccbar  37184  imadifss  37555  finixpnum  37565  matunitlindflem1  37576  mblfinlem4  37620  prdsbnd  37753  heibor1lem  37769  sspadd2  39773  pclfinN  39857  dochdmj1  41347  mzpcompact2lem  42707  eldioph2  42718  eldioph4b  42767  ttac  42993  pwssplit4  43046  isnumbasgrplem2  43061  isnumbasabl  43063  dfacbasgrp  43065  algsca  43138  algvsca  43139  fiuneneq  43153  tfsconcatrnss12  43311  rclexi  43577  rtrclex  43579  trclubgNEW  43580  trclexi  43582  rtrclexi  43583  cnvrcl0  43587  cnvtrcl0  43588  dfrtrcl5  43591  trrelsuperrel2dg  43633  dfrcl2  43636  relexp0a  43678  relexpaddss  43680  trclimalb2  43688  frege109d  43719  frege131d  43726  isotone1  44010  grumnudlem  44254  rnwf  44914  iblsplit  45887  fourierdlem46  46073  sge0resplit  46327  sge0split  46330  sge0splitmpt  46332  sge0xaddlem1  46354  sbgoldbo  47661  dfnbgrss  47724  gsumsplit2f  47903  setrec1  48783  elpglem2  48804