Theorem ssun2 4142

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 4141	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4121	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3995	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3912   ⊆ wss 3914

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-un 3919  df-ss 3931

This theorem is referenced by:  ssun4  4144  elun2  4146  nsspssun  4231  unv  4362  un00  4408  pwunss  4581  snsspr2  4779  snsstp3  4782  fvrn0  6888  riotassuni  7384  ovima0  7568  unexb  7723  unexbOLD  7724  difex2  7736  rnexg  7878  xpord2indlem  8126  xpord3inddlem  8133  fnsuppres  8170  brtpos0  8212  frrlem14  8278  oaabs2  8613  domunsncan  9041  mapunen  9110  ac6sfi  9231  unfir  9257  domunfican  9272  iunfi  9294  elfiun  9381  dffi3  9382  hartogslem1  9495  unwdomg  9537  unxpwdom2  9541  unxpwdom  9542  trcl  9681  unwf  9763  rankunb  9803  r0weon  9965  infxpenlem  9966  alephfplem4  10060  dju1dif  10126  cdainflem  10141  infdju  10160  cfsuc  10210  fin1a2lem10  10362  axdc3lem4  10406  ttukeylem7  10468  fpwwe2lem12  10595  canthp1lem2  10606  gchac  10634  wunrn  10682  wunex2  10691  inar1  10728  pnfxr  11228  ltrelxr  11235  un0mulcl  12476  fzdifsuc  13545  seqexw  13982  hashbclem  14417  hashf1lem1  14420  ccatrn  14554  trclublem  14961  relexprng  15012  fsumsplit  15707  o1fsum  15779  incexclem  15802  fprodsplit  15932  vdwlem5  16956  vdwlem8  16959  ramcl2  16987  srnginvl  17276  lmodvsca  17292  ipssca  17303  ipsvsca  17304  ipsip  17305  phlvsca  17313  phlip  17314  odrngtset  17370  odrngle  17371  odrngds  17372  prdssca  17419  prdsvsca  17423  prdsip  17424  prdsle  17425  prdsds  17427  prdstset  17429  prdshom  17430  prdsco  17431  imasds  17476  imassca  17482  imasvsca  17483  imasip  17484  imastset  17485  imasle  17486  mreexexlemd  17605  mreexexlem2d  17606  mreexexlem3d  17607  drsdirfi  18266  ipolerval  18491  psdmrn  18532  dirge  18562  grpinvfval  18910  mulgfval  19001  gsumzsplit  19857  gsumsplit2  19859  gsumzunsnd  19886  gsum2dlem2  19901  dprdfadd  19952  dmdprdsplit2lem  19977  dmdprdsplit2  19978  dmdprdsplit  19979  dprdsplit  19980  ablfac1eulem  20004  pgpfaclem1  20013  lspun  20893  lbsextlem2  21069  lbsextlem3  21070  lbsextlem4  21071  cnfldcj  21273  cnfldtset  21274  cnfldle  21275  cnfldds  21276  cnfldunif  21277  cnfldcjOLD  21286  cnfldtsetOLD  21287  cnfldleOLD  21288  cnflddsOLD  21289  cnfldunifOLD  21290  psrsca  21856  psrvscafval  21857  mplsubglem  21908  mplcoe5  21947  opsrtoslem2  21963  ordtbas2  23078  ordtbas  23079  ordtopn1  23081  ordtopn2  23082  leordtval2  23099  icomnfordt  23103  iooordt  23104  perfcls  23252  uncmp  23290  fiuncmp  23291  2ndcdisj2  23344  comppfsc  23419  1stckgenlem  23440  1stckgen  23441  ptbasin  23464  ptbasfi  23468  dfac14lem  23504  dfac14  23505  ptuncnv  23694  ptunhmeo  23695  ptcmpfi  23700  fbun  23727  filconn  23770  isufil2  23795  ufprim  23796  fin1aufil  23819  flimclslem  23871  flimfnfcls  23915  tmdgsum  23982  tsmsgsum  24026  tsmssplit  24039  tsmsxplem1  24040  trust  24117  prdsdsf  24255  prdsmet  24258  prdsbl  24379  cnmpopc  24822  rrxmetlem  25307  rrxmet  25308  rrxdstprj1  25309  ovolctb2  25393  ovolfiniun  25402  finiunmbl  25445  volfiniun  25448  uniioombllem3  25486  uniioombllem4  25487  mbfres2  25546  itg2splitlem  25649  itg2split  25650  itgsplit  25737  limcvallem  25772  ellimc2  25778  limccnp  25792  limccnp2  25793  limcco  25794  dvmptfsum  25879  lhop2  25920  lhop  25921  mdegcl  25974  elply2  26101  elplyd  26107  ply1term  26109  ply0  26113  plyaddlem1  26118  plymullem1  26119  plymullem  26121  mtest  26313  xrlimcnp  26878  jensen  26899  fsumharmonic  26922  chtdif  27068  lgsdir2lem3  27238  lgsquadlem2  27292  dchrisumlem2  27401  dchrisum0lem1b  27426  dchrisum0lem1  27427  pntrlog2bndlem6  27494  pntlemf  27516  nosupinfsep  27644  noetasuplem4  27648  noetalem1  27653  cofcutrtime  27835  addsuniflem  27908  addsbday  27924  negsval  27931  mulsproplem12  28030  mulsproplem13  28031  mulsproplem14  28032  mulsuniflem  28052  mulsass  28069  precsexlem10  28118  bdayn0p1  28258  shsleji  31299  shsval2i  31316  ssjo  31376  sshhococi  31475  gsumle  33038  symgcom  33040  elrgspnsubrunlem1  33198  elrgspnsubrunlem2  33199  elrspunsn  33400  idlsrgtset  33479  rtelextdg2  33717  constrextdg2lem  33738  esumsplit  34043  measun  34201  aean  34234  sxbrsigalem2  34277  bnj970  34937  bnj1137  34985  subfacp1lem2a  35167  subfacp1lem3  35169  subfacp1lem5  35171  erdszelem8  35185  kur14lem7  35199  cvmliftlem10  35281  mrsubvr  35498  refssfne  36346  topjoin  36353  tailf  36363  bj-unrab  36914  bj-2upln1upl  37012  bj-ccinftyssccbar  37206  imadifss  37589  finixpnum  37599  matunitlindflem1  37610  mblfinlem4  37654  prdsbnd  37787  heibor1lem  37803  sspadd2  39810  pclfinN  39894  dochdmj1  41384  mzpcompact2lem  42739  eldioph2  42750  eldioph4b  42799  ttac  43025  pwssplit4  43078  isnumbasgrplem2  43093  isnumbasabl  43095  dfacbasgrp  43097  algsca  43166  algvsca  43167  fiuneneq  43181  tfsconcatrnss12  43338  rclexi  43604  rtrclex  43606  trclubgNEW  43607  trclexi  43609  rtrclexi  43610  cnvrcl0  43614  cnvtrcl0  43615  dfrtrcl5  43618  trrelsuperrel2dg  43660  dfrcl2  43663  relexp0a  43705  relexpaddss  43707  trclimalb2  43715  frege109d  43746  frege131d  43753  isotone1  44037  grumnudlem  44274  rnwf  44956  iblsplit  45964  fourierdlem46  46150  sge0resplit  46404  sge0split  46407  sge0splitmpt  46409  sge0xaddlem1  46431  sbgoldbo  47788  dfnbgrss  47852  gsumsplit2f  48168  setrec1  49680  elpglem2  49701