Theorem ssun2 4174

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 4173	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4154	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 4019	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3947   ⊆ wss 3949

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-un 3954  df-in 3956  df-ss 3966

This theorem is referenced by:  ssun4  4176  elun2  4178  nsspssun  4258  unv  4396  un00  4443  pwunss  4621  snsspr2  4819  snsstp3  4822  fvrn0  6922  riotassuni  7406  ovima0  7586  unexb  7735  difex2  7747  rnexg  7895  xpord2indlem  8133  xpord3inddlem  8140  fnsuppres  8176  brtpos0  8218  frrlem14  8284  wfrlem16OLD  8324  oaabs2  8648  domunsncan  9072  mapunen  9146  ac6sfi  9287  unfir  9314  domunfican  9320  iunfi  9340  elfiun  9425  dffi3  9426  hartogslem1  9537  unwdomg  9579  unxpwdom2  9583  unxpwdom  9584  trcl  9723  unwf  9805  rankunb  9845  r0weon  10007  infxpenlem  10008  alephfplem4  10102  dju1dif  10167  cdainflem  10182  infdju  10203  cfsuc  10252  fin1a2lem10  10404  axdc3lem4  10448  ttukeylem7  10510  fpwwe2lem12  10637  canthp1lem2  10648  gchac  10676  wunrn  10724  wunex2  10733  inar1  10770  pnfxr  11268  ltrelxr  11275  un0mulcl  12506  fzdifsuc  13561  seqexw  13982  hashbclem  14411  hashf1lem1  14415  hashf1lem1OLD  14416  ccatrn  14539  trclublem  14942  relexprng  14993  fsumsplit  15687  o1fsum  15759  incexclem  15782  fprodsplit  15910  vdwlem5  16918  vdwlem8  16921  ramcl2  16949  srnginvl  17258  lmodvsca  17274  ipssca  17285  ipsvsca  17286  ipsip  17287  phlvsca  17295  phlip  17296  odrngtset  17352  odrngle  17353  odrngds  17354  prdssca  17402  prdsvsca  17406  prdsip  17407  prdsle  17408  prdsds  17410  prdstset  17412  prdshom  17413  prdsco  17414  imasds  17459  imassca  17465  imasvsca  17466  imasip  17467  imastset  17468  imasle  17469  mreexexlemd  17588  mreexexlem2d  17589  mreexexlem3d  17590  drsdirfi  18258  ipolerval  18485  psdmrn  18526  dirge  18556  grpinvfval  18863  mulgfval  18952  gsumzsplit  19795  gsumsplit2  19797  gsumzunsnd  19824  gsum2dlem2  19839  dprdfadd  19890  dmdprdsplit2lem  19915  dmdprdsplit2  19916  dmdprdsplit  19917  dprdsplit  19918  ablfac1eulem  19942  pgpfaclem1  19951  lspun  20598  lbsextlem2  20772  lbsextlem3  20773  lbsextlem4  20774  cnfldcj  20951  cnfldtset  20952  cnfldle  20953  cnfldds  20954  cnfldunif  20955  psrbagaddclOLD  21482  psrsca  21508  psrvscafval  21509  mplsubglem  21558  mplcoe5  21595  opsrtoslem2  21617  ordtbas2  22695  ordtbas  22696  ordtopn1  22698  ordtopn2  22699  leordtval2  22716  icomnfordt  22720  iooordt  22721  perfcls  22869  uncmp  22907  fiuncmp  22908  2ndcdisj2  22961  comppfsc  23036  1stckgenlem  23057  1stckgen  23058  ptbasin  23081  ptbasfi  23085  dfac14lem  23121  dfac14  23122  ptuncnv  23311  ptunhmeo  23312  ptcmpfi  23317  fbun  23344  filconn  23387  isufil2  23412  ufprim  23413  fin1aufil  23436  flimclslem  23488  flimfnfcls  23532  tmdgsum  23599  tsmsgsum  23643  tsmssplit  23656  tsmsxplem1  23657  trust  23734  prdsdsf  23873  prdsmet  23876  prdsbl  24000  cnmpopc  24444  rrxmetlem  24924  rrxmet  24925  rrxdstprj1  24926  ovolctb2  25009  ovolfiniun  25018  finiunmbl  25061  volfiniun  25064  uniioombllem3  25102  uniioombllem4  25103  mbfres2  25162  itg2splitlem  25266  itg2split  25267  itgsplit  25353  limcvallem  25388  ellimc2  25394  limccnp  25408  limccnp2  25409  limcco  25410  dvmptfsum  25492  lhop2  25532  lhop  25533  mdegcl  25587  elply2  25710  elplyd  25716  ply1term  25718  ply0  25722  plyaddlem1  25727  plymullem1  25728  plymullem  25730  mtest  25916  xrlimcnp  26473  jensen  26493  fsumharmonic  26516  chtdif  26662  lgsdir2lem3  26830  lgsquadlem2  26884  dchrisumlem2  26993  dchrisum0lem1b  27018  dchrisum0lem1  27019  pntrlog2bndlem6  27086  pntlemf  27108  nosupinfsep  27235  noetasuplem4  27239  noetalem1  27244  cofcutrtime  27416  addsuniflem  27487  negsval  27503  mulsproplem12  27586  mulsproplem13  27587  mulsproplem14  27588  mulsuniflem  27607  mulsass  27624  precsexlem10  27665  shsleji  30654  shsval2i  30671  ssjo  30731  sshhococi  30830  gsumle  32273  symgcom  32275  elrspunsn  32578  idlsrgtset  32653  esumsplit  33082  measun  33240  aean  33273  sxbrsigalem2  33316  bnj970  33989  bnj1137  34037  subfacp1lem2a  34202  subfacp1lem3  34204  subfacp1lem5  34206  erdszelem8  34220  kur14lem7  34234  cvmliftlem10  34316  mrsubvr  34533  gg-cnfldcj  35223  gg-cnfldtset  35224  gg-cnfldle  35225  gg-cnfldds  35226  gg-cnfldunif  35227  refssfne  35291  topjoin  35298  tailf  35308  bj-unrab  35854  bj-2upln1upl  35953  bj-ccinftyssccbar  36147  imadifss  36511  finixpnum  36521  matunitlindflem1  36532  mblfinlem4  36576  prdsbnd  36709  heibor1lem  36725  sspadd2  38735  pclfinN  38819  dochdmj1  40309  mzpcompact2lem  41537  eldioph2  41548  eldioph4b  41597  ttac  41823  pwssplit4  41879  isnumbasgrplem2  41894  isnumbasabl  41896  dfacbasgrp  41898  algsca  41971  algvsca  41972  fiuneneq  41987  tfsconcatrnss12  42147  rclexi  42414  rtrclex  42416  trclubgNEW  42417  trclexi  42419  rtrclexi  42420  cnvrcl0  42424  cnvtrcl0  42425  dfrtrcl5  42428  trrelsuperrel2dg  42470  dfrcl2  42473  relexp0a  42515  relexpaddss  42517  trclimalb2  42525  frege109d  42556  frege131d  42563  isotone1  42847  grumnudlem  43092  iblsplit  44730  fourierdlem46  44916  sge0resplit  45170  sge0split  45173  sge0splitmpt  45175  sge0xaddlem1  45197  sbgoldbo  46503  gsumsplit2f  46638  setrec1  47784  elpglem2  47805