Theorem ssun2 4151

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 4150	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4131	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4005	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3936   ⊆ wss 3938

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 2795

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 2802  df-cleq 2816  df-clel 2895  df-nfc 2965  df-v 3498  df-un 3943  df-in 3945  df-ss 3954

This theorem is referenced by:  ssun4  4153  elun2  4155  nsspssun  4236  unv  4351  un00  4396  pwunss  4561  snsspr2  4750  snsstp3  4753  fvrn0  6700  riotassuni  7156  ovima0  7329  unexb  7473  difex2  7484  rnexg  7616  fnsuppres  7859  brtpos0  7901  wfrlem16  7972  oaabs2  8274  domunsncan  8619  mapunen  8688  ac6sfi  8764  unfir  8788  domunfican  8793  iunfi  8814  elfiun  8896  dffi3  8897  hartogslem1  9008  unwdomg  9050  unxpwdom2  9054  unxpwdom  9055  trcl  9172  unwf  9241  rankunb  9281  r0weon  9440  infxpenlem  9441  alephfplem4  9535  dju1dif  9600  cdainflem  9615  infdju  9632  cfsuc  9681  fin1a2lem10  9833  axdc3lem4  9877  ttukeylem7  9939  fpwwe2lem13  10066  canthp1lem2  10077  gchac  10105  wunrn  10153  wunex2  10162  inar1  10199  pnfxr  10697  ltrelxr  10704  un0mulcl  11934  fzdifsuc  12970  seqexw  13388  hashbclem  13813  hashf1lem1  13816  ccatrn  13945  trclublem  14357  relexprng  14407  fsumsplit  15099  o1fsum  15170  incexclem  15193  fprodsplit  15322  vdwlem5  16323  vdwlem8  16326  ramcl2  16354  srnginvl  16633  lmodvsca  16642  ipssca  16649  ipsvsca  16650  ipsip  16651  phlvsca  16659  phlip  16660  odrngtset  16685  odrngle  16686  odrngds  16687  prdssca  16731  prdsvsca  16735  prdsip  16736  prdsle  16737  prdsds  16739  prdstset  16741  prdshom  16742  prdsco  16743  imasds  16788  imassca  16794  imasvsca  16795  imasip  16796  imastset  16797  imasle  16798  mreexexlemd  16917  mreexexlem2d  16918  mreexexlem3d  16919  drsdirfi  17550  ipolerval  17768  psdmrn  17819  dirge  17849  grpinvfval  18144  mulgfval  18228  gsumzsplit  19049  gsumsplit2  19051  gsumzunsnd  19078  gsum2dlem2  19093  dprdfadd  19144  dmdprdsplit2lem  19169  dmdprdsplit2  19170  dmdprdsplit  19171  dprdsplit  19172  ablfac1eulem  19196  pgpfaclem1  19205  lspun  19761  lbsextlem2  19933  lbsextlem3  19934  lbsextlem4  19935  psrbagaddcl  20152  psrsca  20171  psrvscafval  20172  mplsubglem  20216  mplcoe5  20251  opsrtoslem2  20267  cnfldcj  20554  cnfldtset  20555  cnfldle  20556  cnfldds  20557  cnfldunif  20558  ordtbas2  21801  ordtbas  21802  ordtopn1  21804  ordtopn2  21805  leordtval2  21822  icomnfordt  21826  iooordt  21827  perfcls  21975  uncmp  22013  fiuncmp  22014  2ndcdisj2  22067  comppfsc  22142  1stckgenlem  22163  1stckgen  22164  ptbasin  22187  ptbasfi  22191  dfac14lem  22227  dfac14  22228  ptuncnv  22417  ptunhmeo  22418  ptcmpfi  22423  fbun  22450  filconn  22493  isufil2  22518  ufprim  22519  fin1aufil  22542  flimclslem  22594  flimfnfcls  22638  tmdgsum  22705  tsmsgsum  22749  tsmssplit  22762  tsmsxplem1  22763  trust  22840  prdsdsf  22979  prdsmet  22982  prdsbl  23103  cnmpopc  23534  rrxmetlem  24012  rrxmet  24013  rrxdstprj1  24014  ovolctb2  24095  ovolfiniun  24104  finiunmbl  24147  volfiniun  24150  uniioombllem3  24188  uniioombllem4  24189  mbfres2  24248  itg2splitlem  24351  itg2split  24352  itgsplit  24438  limcvallem  24471  ellimc2  24477  limccnp  24491  limccnp2  24492  limcco  24493  dvmptfsum  24574  lhop2  24614  lhop  24615  mdegcl  24665  elply2  24788  elplyd  24794  ply1term  24796  ply0  24800  plyaddlem1  24805  plymullem1  24806  plymullem  24808  mtest  24994  xrlimcnp  25548  jensen  25568  fsumharmonic  25591  chtdif  25737  lgsdir2lem3  25905  lgsquadlem2  25959  dchrisumlem2  26068  dchrisum0lem1b  26093  dchrisum0lem1  26094  pntrlog2bndlem6  26161  pntlemf  26183  shsleji  29149  shsval2i  29166  ssjo  29226  sshhococi  29325  gsumle  30727  symgcom  30729  esumsplit  31314  measun  31472  aean  31505  sxbrsigalem2  31546  bnj970  32221  bnj1137  32269  subfacp1lem2a  32429  subfacp1lem3  32431  subfacp1lem5  32433  erdszelem8  32447  kur14lem7  32461  cvmliftlem10  32543  mrsubvr  32760  frrlem14  33138  noetalem3  33221  refssfne  33708  topjoin  33715  tailf  33725  bj-unrab  34246  bj-2upln1upl  34338  bj-ccinftyssccbar  34502  imadifss  34869  finixpnum  34879  matunitlindflem1  34890  mblfinlem4  34934  prdsbnd  35073  heibor1lem  35089  sspadd2  36954  pclfinN  37038  dochdmj1  38528  mzpcompact2lem  39355  eldioph2  39366  eldioph4b  39415  ttac  39640  pwssplit4  39696  isnumbasgrplem2  39711  isnumbasabl  39713  dfacbasgrp  39715  algsca  39788  algvsca  39789  fiuneneq  39804  rclexi  39982  rtrclex  39984  trclubgNEW  39985  trclexi  39987  rtrclexi  39988  cnvrcl0  39992  cnvtrcl0  39993  dfrtrcl5  39996  trrelsuperrel2dg  40023  dfrcl2  40026  relexp0a  40068  relexpaddss  40070  trclimalb2  40078  frege109d  40109  frege131d  40116  isotone1  40405  grumnudlem  40628  iblsplit  42258  fourierdlem46  42444  sge0resplit  42695  sge0split  42698  sge0splitmpt  42700  sge0xaddlem1  42722  sbgoldbo  43959  gsumsplit2f  44094  setrec1  44801  elpglem2  44821