Theorem ssun2 4131

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 4130	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4111	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3984	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3902   ⊆ wss 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1823  ax-4 1837  ax-5 1938  ax-6 1995  ax-7 2036  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1571  df-ex 1808  df-sb 2095  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-un 3909  df-ss 3921

This theorem is referenced by:  ssun4  4133  elun2  4135  nsspssun  4220  unv  4355  un00  4363  pwunss  4579  snsspr2  4780  snsstp3  4783  imadifssran  6202  fvrn0  6909  riotassuni  7407  ovima0  7589  unexb  7745  unexbOLD  7746  difex2  7758  rnexg  7898  xpord2indlem  8142  xpord3inddlem  8149  fnsuppres  8186  brtpos0  8228  frrlem14  8295  oaabs2  8634  domunsncan  9064  mapunen  9133  ac6sfi  9243  unfir  9267  domunfican  9280  iunfi  9299  elfiun  9389  dffi3  9390  hartogslem1  9503  unwdomg  9545  unxpwdom2  9549  unxpwdom  9550  trcl  9696  unwf  9781  rankunb  9821  r0weon  9995  infxpenlem  9996  alephfplem4  10090  dju1dif  10155  cdainflem  10170  infdju  10189  cfsuc  10240  fin1a2lem10  10392  axdc3lem4  10436  ttukeylem7  10498  fpwwe2lem12  10626  canthp1lem2  10637  gchac  10665  wunrn  10713  wunex2  10722  inar1  10759  pnfxr  11262  ltrelxr  11269  un0mulcl  12537  fzdifsuc  13611  seqexw  14052  hashbclem  14488  hashf1lem1  14491  ccatrn  14626  trclublem  15031  relexprng  15082  fsumsplit  15791  o1fsum  15864  incexclem  15889  fprodsplit  16019  vdwlem5  17044  vdwlem8  17047  ramcl2  17075  srnginvl  17365  lmodvsca  17381  ipssca  17392  ipsvsca  17393  ipsip  17394  phlvsca  17402  phlip  17403  odrngtset  17459  odrngle  17460  odrngds  17461  prdssca  17508  prdsvsca  17512  prdsip  17513  prdsle  17514  prdsds  17516  prdstset  17518  prdshom  17519  prdsco  17520  imasds  17566  imassca  17572  imasvsca  17573  imasip  17574  imastset  17575  imasle  17576  mreexexlemd  17699  mreexexlem2d  17700  mreexexlem3d  17701  drsdirfi  18360  ipolerval  18587  psdmrn  18628  dirge  18658  grpinvfval  19044  mulgfval  19134  gsumzsplit  19996  gsumsplit2  19998  gsumzunsnd  20025  gsum2dlem2  20040  dprdfadd  20091  dmdprdsplit2lem  20116  dmdprdsplit2  20117  dmdprdsplit  20118  dprdsplit  20119  ablfac1eulem  20143  pgpfaclem1  20152  gsumle  20214  lspun  21087  lbsextlem2  21262  lbsextlem3  21263  lbsextlem4  21264  cnfldcj  21510  cnfldtset  21511  cnfldle  21512  cnfldds  21513  cnfldunif  21514  psrsca  22076  psrvscafval  22077  mplsubglem  22127  mplcoe5  22170  opsrtoslem2  22186  ordtbas2  23327  ordtbas  23328  ordtopn1  23330  ordtopn2  23331  leordtval2  23348  icomnfordt  23352  iooordt  23353  perfcls  23501  uncmp  23539  fiuncmp  23540  2ndcdisj2  23593  comppfsc  23668  1stckgenlem  23689  1stckgen  23690  ptbasin  23713  ptbasfi  23717  dfac14lem  23753  dfac14  23754  ptuncnv  23943  ptunhmeo  23944  ptcmpfi  23949  fbun  23976  filconn  24019  isufil2  24044  ufprim  24045  fin1aufil  24068  flimclslem  24120  flimfnfcls  24164  tmdgsum  24231  tsmsgsum  24275  tsmssplit  24288  tsmsxplem1  24289  trust  24365  prdsdsf  24503  prdsmet  24506  prdsbl  24627  cnmpopc  25066  rrxmetlem  25545  rrxmet  25546  rrxdstprj1  25547  ovolctb2  25630  ovolfiniun  25639  finiunmbl  25682  volfiniun  25685  uniioombllem3  25723  uniioombllem4  25724  mbfres2  25783  itg2splitlem  25886  itg2split  25887  itgsplit  25974  limcvallem  26009  ellimc2  26015  limccnp  26029  limccnp2  26030  limcco  26031  dvmptfsum  26113  lhop2  26153  lhop  26154  mdegcl  26205  elply2  26332  elplyd  26338  ply1term  26340  ply0  26344  plyaddlem1  26349  plymullem1  26350  plymullem  26352  mtest  26543  xrlimcnp  27109  jensen  27129  fsumharmonic  27152  chtdif  27298  lgsdir2lem3  27467  lgsquadlem2  27521  dchrisumlem2  27630  dchrisum0lem1b  27655  dchrisum0lem1  27656  pntrlog2bndlem6  27723  pntlemf  27745  nosupinfsep  27872  noetasuplem4  27876  noetalem1  27881  cofcutrtime  28096  addsuniflem  28170  addbday  28187  negsval  28194  mulsproplem12  28296  mulsproplem13  28297  mulsproplem14  28298  mulsuniflem  28318  mulsass  28335  precsexlem10  28385  bdayn0p1  28538  shsleji  31688  shsval2i  31705  ssjo  31765  sshhococi  31864  symgcom  33369  elrgspnsubrunlem1  33533  elrgspnsubrunlem2  33534  elrspunsn  33703  idlsrgtset  33764  vieta  33936  rtelextdg2  34083  constrextdg2lem  34104  esumsplit  34409  measun  34567  aean  34600  sxbrsigalem2  34642  bnj970  35301  bnj1137  35349  subfacp1lem2a  35626  subfacp1lem3  35628  subfacp1lem5  35630  erdszelem8  35644  kur14lem7  35658  cvmliftlem10  35740  mrsubvr  35957  refssfne  36813  topjoin  36820  tailf  36830  ttcuniun  36965  ttciunun  36966  bj-unrab  37506  bj-2upln1upl  37604  bj-ccinftyssccbar  37806  imadifss  38190  finixpnum  38200  matunitlindflem1  38211  mblfinlem4  38255  prdsbnd  38388  heibor1lem  38404  sspadd2  40536  pclfinN  40620  dochdmj1  42110  mzpcompact2lem  43430  eldioph2  43441  eldioph4b  43486  ttac  43711  pwssplit4  43764  isnumbasgrplem2  43779  isnumbasabl  43781  dfacbasgrp  43783  algsca  43852  algvsca  43853  fiuneneq  43867  tfsconcatrnss12  44024  rclexi  44289  rtrclex  44291  trclubgNEW  44292  trclexi  44294  rtrclexi  44295  cnvrcl0  44299  cnvtrcl0  44300  dfrtrcl5  44303  trrelsuperrel2dg  44345  dfrcl2  44348  relexp0a  44390  relexpaddss  44392  trclimalb2  44400  frege109d  44431  frege131d  44438  isotone1  44722  grumnudlem  44943  rnwf  45623  iblsplit  46628  fourierdlem46  46814  sge0resplit  47068  sge0split  47071  sge0splitmpt  47073  sge0xaddlem1  47095  sbgoldbo  48497  dfnbgrss  48562  gsumsplit2f  48890  setrec1  50414  elpglem2  50435