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 3986	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

This proof depends on syntax axioms:   ∪ cun 3904   ⊆ wss 3906

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-un 3911  df-ss 3923

This theorem is used by:  ssun4  4134  elun2  4136  nsspssun  4221  unv  4356  un00  4364  pwunss  4582  snsspr2  4783  snsstp3  4786  imadifssran  6204  fvrn0  6913  riotassuni  7413  ovima0  7595  unexb  7750  difex2  7761  rnexg  7901  xpord2indlem  8145  xpord3inddlem  8152  fnsuppres  8189  brtpos0  8231  frrlem14  8298  oaabs2  8637  domunsncan  9068  mapunen  9137  ac6sfi  9247  unfir  9271  domunfican  9284  iunfi  9303  elfiun  9393  dffi3  9394  hartogslem1  9507  unwdomg  9549  unxpwdom2  9553  unxpwdom  9554  trcl  9700  unwf  9785  rankunb  9825  r0weon  10008  infxpenlem  10009  alephfplem4  10103  dju1dif  10168  cdainflem  10183  infdju  10202  cfsuc  10252  fin1a2lem10  10404  axdc3lem4  10448  ttukeylem7  10510  fpwwe2lem12  10638  canthp1lem2  10649  gchac  10677  wunrn  10725  wunex2  10734  inar1  10771  pnfxr  11274  ltrelxr  11281  un0mulcl  12549  fzdifsuc  13625  seqexw  14067  hashbclem  14503  hashf1lem1  14506  ccatrn  14641  trclublem  15052  relexprng  15103  fsumsplit  15811  o1fsum  15884  incexclem  15909  fprodsplit  16039  vdwlem5  17063  vdwlem8  17066  ramcl2  17094  srnginvl  17384  lmodvsca  17400  ipssca  17411  ipsvsca  17412  ipsip  17413  phlvsca  17421  phlip  17422  odrngtset  17478  odrngle  17479  odrngds  17480  prdssca  17527  prdsvsca  17531  prdsip  17532  prdsle  17533  prdsds  17535  prdstset  17537  prdshom  17538  prdsco  17539  imasds  17585  imassca  17591  imasvsca  17592  imasip  17593  imastset  17594  imasle  17595  mreexexlemd  17718  mreexexlem2d  17719  mreexexlem3d  17720  drsdirfi  18379  ipolerval  18606  psdmrn  18647  dirge  18677  grpinvfval  19069  mulgfval  19159  gsumzsplit  20021  gsumsplit2  20023  gsumzunsnd  20050  gsum2dlem2  20065  dprdfadd  20116  dmdprdsplit2lem  20141  dmdprdsplit2  20142  dmdprdsplit  20143  dprdsplit  20144  ablfac1eulem  20168  pgpfaclem1  20177  gsumle  20239  lspun  21138  lbsextlem2  21313  lbsextlem3  21314  lbsextlem4  21315  cnfldcj  21561  cnfldtset  21562  cnfldle  21563  cnfldds  21564  cnfldunif  21565  psrsca  22127  psrvscafval  22128  mplsubglem  22178  mplcoe5  22221  opsrtoslem2  22237  ordtbas2  23378  ordtbas  23379  ordtopn1  23381  ordtopn2  23382  leordtval2  23399  icomnfordt  23403  iooordt  23404  perfcls  23552  uncmp  23590  fiuncmp  23591  2ndcdisj2  23645  comppfsc  23720  1stckgenlem  23741  1stckgen  23742  ptbasin  23765  ptbasfi  23769  dfac14lem  23805  dfac14  23806  ptuncnv  23995  ptunhmeo  23996  ptcmpfi  24001  fbun  24028  filconn  24071  isufil2  24096  ufprim  24097  fin1aufil  24120  flimclslem  24172  flimfnfcls  24216  tmdgsum  24283  tsmsgsum  24327  tsmssplit  24340  tsmsxplem1  24341  trust  24417  prdsdsf  24555  prdsmet  24558  prdsbl  24679  cnmpopc  25118  rrxmetlem  25597  rrxmet  25598  rrxdstprj1  25599  ovolctb2  25682  ovolfiniun  25691  finiunmbl  25734  volfiniun  25737  uniioombllem3  25775  uniioombllem4  25776  mbfres2  25835  itg2splitlem  25938  itg2split  25939  itgsplit  26026  limcvallem  26061  ellimc2  26067  limccnp  26081  limccnp2  26082  limcco  26083  dvmptfsum  26165  lhop2  26205  lhop  26206  mdegcl  26257  elply2  26384  elplyd  26390  ply1term  26392  ply0  26396  plyaddlem1  26401  plymullem1  26402  plymullem  26404  mtest  26598  xrlimcnp  27164  jensen  27184  fsumharmonic  27207  chtdif  27353  lgsdir2lem3  27522  lgsquadlem2  27576  dchrisumlem2  27685  dchrisum0lem1b  27710  dchrisum0lem1  27711  pntrlog2bndlem6  27778  pntlemf  27800  nosupinfsep  27927  noetasuplem4  27931  noetalem1  27936  cofcutrtime  28151  addsuniflem  28225  addbday  28242  negsval  28249  mulsproplem12  28351  mulsproplem13  28352  mulsproplem14  28353  mulsuniflem  28373  mulsass  28390  precsexlem10  28440  bdayn0p1  28593  shsleji  31769  shsval2i  31786  ssjo  31846  sshhococi  31945  symgcom  33443  elrgspnsubrunlem1  33607  elrgspnsubrunlem2  33608  elrspunsn  33777  idlsrgtset  33838  vieta  34010  rtelextdg2  34157  constrextdg2lem  34178  esumsplit  34483  measun  34642  aean  34675  sxbrsigalem2  34717  bnj970  35376  bnj1137  35424  subfacp1lem2a  35685  subfacp1lem3  35687  subfacp1lem5  35689  erdszelem8  35703  kur14lem7  35717  cvmliftlem10  35799  mrsubvr  36016  refssfne  36902  topjoin  36909  tailf  36919  ttcuniun  37054  ttciunun  37055  bj-unrab  37595  bj-2upln1upl  37693  bj-ccinftyssccbar  37895  imadifss  38279  finixpnum  38289  matunitlindflem1  38300  mblfinlem4  38344  prdsbnd  38477  heibor1lem  38493  sspadd2  40623  pclfinN  40707  dochdmj1  42197  mzpcompact2lem  43515  eldioph2  43526  eldioph4b  43571  ttac  43796  pwssplit4  43849  isnumbasgrplem2  43864  isnumbasabl  43866  dfacbasgrp  43868  algsca  43937  algvsca  43938  fiuneneq  43952  tfsconcatrnss12  44109  rclexi  44374  rtrclex  44376  trclubgNEW  44377  trclexi  44379  rtrclexi  44380  cnvrcl0  44384  cnvtrcl0  44385  dfrtrcl5  44388  trrelsuperrel2dg  44430  dfrcl2  44433  relexp0a  44475  relexpaddss  44477  trclimalb2  44485  frege109d  44516  frege131d  44523  isotone1  44807  grumnudlem  45028  rnwf  45708  iblsplit  46713  fourierdlem46  46899  sge0resplit  47153  sge0split  47156  sge0splitmpt  47158  sge0xaddlem1  47180  sbgoldbo  48585  dfnbgrss  48650  gsumsplit2f  48978  setrec1  50502  elpglem2  50523