Theorem ssun2 4132

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

Syntax hints:   ∪ cun 3903   ⊆ wss 3905

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-un 3910  df-ss 3922

This theorem is referenced by:  ssun4  4134  elun2  4136  nsspssun  4221  unv  4356  un00  4364  pwunss  4580  snsspr2  4781  snsstp3  4784  imadifssran  6202  fvrn0  6909  riotassuni  7407  ovima0  7589  unexb  7744  difex2  7755  rnexg  7895  xpord2indlem  8139  xpord3inddlem  8146  fnsuppres  8183  brtpos0  8225  frrlem14  8292  oaabs2  8631  domunsncan  9061  mapunen  9130  ac6sfi  9240  unfir  9264  domunfican  9277  iunfi  9296  elfiun  9386  dffi3  9387  hartogslem1  9500  unwdomg  9542  unxpwdom2  9546  unxpwdom  9547  trcl  9693  unwf  9778  rankunb  9818  r0weon  9992  infxpenlem  9993  alephfplem4  10087  dju1dif  10152  cdainflem  10167  infdju  10186  cfsuc  10236  fin1a2lem10  10388  axdc3lem4  10432  ttukeylem7  10494  fpwwe2lem12  10622  canthp1lem2  10633  gchac  10661  wunrn  10709  wunex2  10718  inar1  10755  pnfxr  11258  ltrelxr  11265  un0mulcl  12533  fzdifsuc  13608  seqexw  14049  hashbclem  14485  hashf1lem1  14488  ccatrn  14623  trclublem  15028  relexprng  15079  fsumsplit  15788  o1fsum  15861  incexclem  15886  fprodsplit  16016  vdwlem5  17040  vdwlem8  17043  ramcl2  17071  srnginvl  17361  lmodvsca  17377  ipssca  17388  ipsvsca  17389  ipsip  17390  phlvsca  17398  phlip  17399  odrngtset  17455  odrngle  17456  odrngds  17457  prdssca  17504  prdsvsca  17508  prdsip  17509  prdsle  17510  prdsds  17512  prdstset  17514  prdshom  17515  prdsco  17516  imasds  17562  imassca  17568  imasvsca  17569  imasip  17570  imastset  17571  imasle  17572  mreexexlemd  17695  mreexexlem2d  17696  mreexexlem3d  17697  drsdirfi  18356  ipolerval  18583  psdmrn  18624  dirge  18654  grpinvfval  19040  mulgfval  19130  gsumzsplit  19992  gsumsplit2  19994  gsumzunsnd  20021  gsum2dlem2  20036  dprdfadd  20087  dmdprdsplit2lem  20112  dmdprdsplit2  20113  dmdprdsplit  20114  dprdsplit  20115  ablfac1eulem  20139  pgpfaclem1  20148  gsumle  20210  lspun  21108  lbsextlem2  21283  lbsextlem3  21284  lbsextlem4  21285  cnfldcj  21531  cnfldtset  21532  cnfldle  21533  cnfldds  21534  cnfldunif  21535  psrsca  22097  psrvscafval  22098  mplsubglem  22148  mplcoe5  22191  opsrtoslem2  22207  ordtbas2  23348  ordtbas  23349  ordtopn1  23351  ordtopn2  23352  leordtval2  23369  icomnfordt  23373  iooordt  23374  perfcls  23522  uncmp  23560  fiuncmp  23561  2ndcdisj2  23614  comppfsc  23689  1stckgenlem  23710  1stckgen  23711  ptbasin  23734  ptbasfi  23738  dfac14lem  23774  dfac14  23775  ptuncnv  23964  ptunhmeo  23965  ptcmpfi  23970  fbun  23997  filconn  24040  isufil2  24065  ufprim  24066  fin1aufil  24089  flimclslem  24141  flimfnfcls  24185  tmdgsum  24252  tsmsgsum  24296  tsmssplit  24309  tsmsxplem1  24310  trust  24386  prdsdsf  24524  prdsmet  24527  prdsbl  24648  cnmpopc  25087  rrxmetlem  25566  rrxmet  25567  rrxdstprj1  25568  ovolctb2  25651  ovolfiniun  25660  finiunmbl  25703  volfiniun  25706  uniioombllem3  25744  uniioombllem4  25745  mbfres2  25804  itg2splitlem  25907  itg2split  25908  itgsplit  25995  limcvallem  26030  ellimc2  26036  limccnp  26050  limccnp2  26051  limcco  26052  dvmptfsum  26134  lhop2  26174  lhop  26175  mdegcl  26226  elply2  26353  elplyd  26359  ply1term  26361  ply0  26365  plyaddlem1  26370  plymullem1  26371  plymullem  26373  mtest  26567  xrlimcnp  27133  jensen  27153  fsumharmonic  27176  chtdif  27322  lgsdir2lem3  27491  lgsquadlem2  27545  dchrisumlem2  27654  dchrisum0lem1b  27679  dchrisum0lem1  27680  pntrlog2bndlem6  27747  pntlemf  27769  nosupinfsep  27896  noetasuplem4  27900  noetalem1  27905  cofcutrtime  28120  addsuniflem  28194  addbday  28211  negsval  28218  mulsproplem12  28320  mulsproplem13  28321  mulsproplem14  28322  mulsuniflem  28342  mulsass  28359  precsexlem10  28409  bdayn0p1  28562  shsleji  31722  shsval2i  31739  ssjo  31799  sshhococi  31898  symgcom  33403  elrgspnsubrunlem1  33567  elrgspnsubrunlem2  33568  elrspunsn  33737  idlsrgtset  33798  vieta  33970  rtelextdg2  34117  constrextdg2lem  34138  esumsplit  34443  measun  34601  aean  34634  sxbrsigalem2  34676  bnj970  35335  bnj1137  35383  subfacp1lem2a  35672  subfacp1lem3  35674  subfacp1lem5  35676  erdszelem8  35690  kur14lem7  35704  cvmliftlem10  35786  mrsubvr  36003  refssfne  36869  topjoin  36876  tailf  36886  ttcuniun  37021  ttciunun  37022  bj-unrab  37562  bj-2upln1upl  37660  bj-ccinftyssccbar  37862  imadifss  38246  finixpnum  38256  matunitlindflem1  38267  mblfinlem4  38311  prdsbnd  38444  heibor1lem  38460  sspadd2  40590  pclfinN  40674  dochdmj1  42164  mzpcompact2lem  43482  eldioph2  43493  eldioph4b  43538  ttac  43763  pwssplit4  43816  isnumbasgrplem2  43831  isnumbasabl  43833  dfacbasgrp  43835  algsca  43904  algvsca  43905  fiuneneq  43919  tfsconcatrnss12  44076  rclexi  44341  rtrclex  44343  trclubgNEW  44344  trclexi  44346  rtrclexi  44347  cnvrcl0  44351  cnvtrcl0  44352  dfrtrcl5  44355  trrelsuperrel2dg  44397  dfrcl2  44400  relexp0a  44442  relexpaddss  44444  trclimalb2  44452  frege109d  44483  frege131d  44490  isotone1  44774  grumnudlem  44995  rnwf  45675  iblsplit  46680  fourierdlem46  46866  sge0resplit  47120  sge0split  47123  sge0splitmpt  47125  sge0xaddlem1  47147  sbgoldbo  48552  dfnbgrss  48617  gsumsplit2f  48945  setrec1  50469  elpglem2  50490