Theorem ssun2 4087

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 4086	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4067	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3937	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3864   ⊆ wss 3866

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-or 848  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-un 3871  df-in 3873  df-ss 3883

This theorem is referenced by:  ssun4  4089  elun2  4091  nsspssun  4172  unv  4310  un00  4357  pwunss  4533  snsspr2  4728  snsstp3  4731  fvrn0  6745  riotassuni  7211  ovima0  7387  unexb  7533  difex2  7545  rnexg  7682  fnsuppres  7933  brtpos0  7975  frrlem14  8040  wfrlem16  8070  oaabs2  8374  domunsncan  8745  mapunen  8815  ac6sfi  8915  unfir  8939  domunfican  8944  iunfi  8964  elfiun  9046  dffi3  9047  hartogslem1  9158  unwdomg  9200  unxpwdom2  9204  unxpwdom  9205  trcl  9344  unwf  9426  rankunb  9466  r0weon  9626  infxpenlem  9627  alephfplem4  9721  dju1dif  9786  cdainflem  9801  infdju  9822  cfsuc  9871  fin1a2lem10  10023  axdc3lem4  10067  ttukeylem7  10129  fpwwe2lem12  10256  canthp1lem2  10267  gchac  10295  wunrn  10343  wunex2  10352  inar1  10389  pnfxr  10887  ltrelxr  10894  un0mulcl  12124  fzdifsuc  13172  seqexw  13590  hashbclem  14016  hashf1lem1  14020  hashf1lem1OLD  14021  ccatrn  14146  trclublem  14558  relexprng  14609  fsumsplit  15305  o1fsum  15377  incexclem  15400  fprodsplit  15528  vdwlem5  16538  vdwlem8  16541  ramcl2  16569  srnginvl  16854  lmodvsca  16865  ipssca  16873  ipsvsca  16874  ipsip  16875  phlvsca  16883  phlip  16884  odrngtset  16914  odrngle  16915  odrngds  16916  prdssca  16961  prdsvsca  16965  prdsip  16966  prdsle  16967  prdsds  16969  prdstset  16971  prdshom  16972  prdsco  16973  imasds  17018  imassca  17024  imasvsca  17025  imasip  17026  imastset  17027  imasle  17028  mreexexlemd  17147  mreexexlem2d  17148  mreexexlem3d  17149  drsdirfi  17812  ipolerval  18038  psdmrn  18079  dirge  18109  grpinvfval  18406  mulgfval  18490  gsumzsplit  19312  gsumsplit2  19314  gsumzunsnd  19341  gsum2dlem2  19356  dprdfadd  19407  dmdprdsplit2lem  19432  dmdprdsplit2  19433  dmdprdsplit  19434  dprdsplit  19435  ablfac1eulem  19459  pgpfaclem1  19468  lspun  20024  lbsextlem2  20196  lbsextlem3  20197  lbsextlem4  20198  cnfldcj  20370  cnfldtset  20371  cnfldle  20372  cnfldds  20373  cnfldunif  20374  psrbagaddclOLD  20888  psrsca  20914  psrvscafval  20915  mplsubglem  20961  mplcoe5  20997  opsrtoslem2  21013  ordtbas2  22088  ordtbas  22089  ordtopn1  22091  ordtopn2  22092  leordtval2  22109  icomnfordt  22113  iooordt  22114  perfcls  22262  uncmp  22300  fiuncmp  22301  2ndcdisj2  22354  comppfsc  22429  1stckgenlem  22450  1stckgen  22451  ptbasin  22474  ptbasfi  22478  dfac14lem  22514  dfac14  22515  ptuncnv  22704  ptunhmeo  22705  ptcmpfi  22710  fbun  22737  filconn  22780  isufil2  22805  ufprim  22806  fin1aufil  22829  flimclslem  22881  flimfnfcls  22925  tmdgsum  22992  tsmsgsum  23036  tsmssplit  23049  tsmsxplem1  23050  trust  23127  prdsdsf  23265  prdsmet  23268  prdsbl  23389  cnmpopc  23825  rrxmetlem  24304  rrxmet  24305  rrxdstprj1  24306  ovolctb2  24389  ovolfiniun  24398  finiunmbl  24441  volfiniun  24444  uniioombllem3  24482  uniioombllem4  24483  mbfres2  24542  itg2splitlem  24646  itg2split  24647  itgsplit  24733  limcvallem  24768  ellimc2  24774  limccnp  24788  limccnp2  24789  limcco  24790  dvmptfsum  24872  lhop2  24912  lhop  24913  mdegcl  24967  elply2  25090  elplyd  25096  ply1term  25098  ply0  25102  plyaddlem1  25107  plymullem1  25108  plymullem  25110  mtest  25296  xrlimcnp  25851  jensen  25871  fsumharmonic  25894  chtdif  26040  lgsdir2lem3  26208  lgsquadlem2  26262  dchrisumlem2  26371  dchrisum0lem1b  26396  dchrisum0lem1  26397  pntrlog2bndlem6  26464  pntlemf  26486  shsleji  29451  shsval2i  29468  ssjo  29528  sshhococi  29627  gsumle  31069  symgcom  31071  idlsrgtset  31367  esumsplit  31733  measun  31891  aean  31924  sxbrsigalem2  31965  bnj970  32640  bnj1137  32688  subfacp1lem2a  32855  subfacp1lem3  32857  subfacp1lem5  32859  erdszelem8  32873  kur14lem7  32887  cvmliftlem10  32969  mrsubvr  33186  xpord2ind  33531  xpord3ind  33537  nosupinfsep  33672  noetasuplem4  33676  noetalem1  33681  cofcutrtime  33830  negsval  33860  refssfne  34284  topjoin  34291  tailf  34301  bj-unrab  34851  bj-2upln1upl  34951  bj-ccinftyssccbar  35124  imadifss  35489  finixpnum  35499  matunitlindflem1  35510  mblfinlem4  35554  prdsbnd  35688  heibor1lem  35704  sspadd2  37567  pclfinN  37651  dochdmj1  39141  mzpcompact2lem  40276  eldioph2  40287  eldioph4b  40336  ttac  40561  pwssplit4  40617  isnumbasgrplem2  40632  isnumbasabl  40634  dfacbasgrp  40636  algsca  40709  algvsca  40710  fiuneneq  40725  rclexi  40899  rtrclex  40901  trclubgNEW  40902  trclexi  40904  rtrclexi  40905  cnvrcl0  40909  cnvtrcl0  40910  dfrtrcl5  40913  trrelsuperrel2dg  40956  dfrcl2  40959  relexp0a  41001  relexpaddss  41003  trclimalb2  41011  frege109d  41042  frege131d  41049  isotone1  41335  grumnudlem  41576  iblsplit  43182  fourierdlem46  43368  sge0resplit  43619  sge0split  43622  sge0splitmpt  43624  sge0xaddlem1  43646  sbgoldbo  44912  gsumsplit2f  45047  setrec1  46068  elpglem2  46088