Theorem ssun2 4076

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 4075	. 2 ⊢ 𝐴 ⊆ (𝐴 ∪ 𝐵)
2		uncom 4056	. 2 ⊢ (𝐴 ∪ 𝐵) = (𝐵 ∪ 𝐴)
3	1, 2	sseqtri 3930	1 ⊢ 𝐴 ⊆ (𝐵 ∪ 𝐴)

Syntax hints:   ∪ cun 3863   ⊆ wss 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1781  ax-4 1795  ax-5 1892  ax-6 1951  ax-7 1996  ax-8 2085  ax-9 2093  ax-10 2114  ax-11 2128  ax-12 2143  ax-ext 2771

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1528  df-ex 1766  df-nf 1770  df-sb 2045  df-clab 2778  df-cleq 2790  df-clel 2865  df-nfc 2937  df-v 3442  df-un 3870  df-in 3872  df-ss 3880

This theorem is referenced by:  ssun4  4078  elun2  4080  nsspssun  4160  unv  4275  un00  4314  snsspr2  4661  snsstp3  4664  fvrn0  6573  riotassuni  7021  ovima0  7190  unexb  7335  difex2  7346  rnexg  7477  fnsuppres  7715  brtpos0  7757  wfrlem16  7829  oaabs2  8129  domunsncan  8471  mapunen  8540  ac6sfi  8615  unfir  8639  domunfican  8644  iunfi  8665  elfiun  8747  dffi3  8748  hartogslem1  8859  unwdomg  8901  unxpwdom2  8905  unxpwdom  8906  trcl  9023  unwf  9092  rankunb  9132  r0weon  9291  infxpenlem  9292  alephfplem4  9386  dju1dif  9451  cdainflem  9466  infdju  9483  cfsuc  9532  fin1a2lem10  9684  axdc3lem4  9728  ttukeylem7  9790  fpwwe2lem13  9917  canthp1lem2  9928  gchac  9956  wunrn  10004  wunex2  10013  inar1  10050  pnfxr  10548  ltrelxr  10555  un0mulcl  11785  fzdifsuc  12821  seqexw  13239  hashbclem  13662  hashf1lem1  13665  ccatrn  13791  trclublem  14193  relexprng  14243  fsumsplit  14934  o1fsum  15005  incexclem  15028  fprodsplit  15157  vdwlem5  16154  vdwlem8  16157  ramcl2  16185  srnginvl  16464  lmodvsca  16473  ipssca  16480  ipsvsca  16481  ipsip  16482  phlvsca  16490  phlip  16491  odrngtset  16516  odrngle  16517  odrngds  16518  prdssca  16562  prdsvsca  16566  prdsip  16567  prdsle  16568  prdsds  16570  prdstset  16572  prdshom  16573  prdsco  16574  imasds  16619  imassca  16625  imasvsca  16626  imasip  16627  imastset  16628  imasle  16629  mreexexlemd  16748  mreexexlem2d  16749  mreexexlem3d  16750  drsdirfi  17381  ipolerval  17599  psdmrn  17650  dirge  17680  grpinvfval  17903  mulgfval  17987  gsumzsplit  18771  gsumsplit2  18773  gsumzunsnd  18800  gsum2dlem2  18815  dprdfadd  18863  dmdprdsplit2lem  18888  dmdprdsplit2  18889  dmdprdsplit  18890  dprdsplit  18891  ablfac1eulem  18915  pgpfaclem1  18924  lspun  19453  lbsextlem2  19625  lbsextlem3  19626  lbsextlem4  19627  psrbagaddcl  19842  psrsca  19861  psrvscafval  19862  mplsubglem  19906  mplcoe5  19940  opsrtoslem2  19956  cnfldcj  20238  cnfldtset  20239  cnfldle  20240  cnfldds  20241  cnfldunif  20242  ordtbas2  21487  ordtbas  21488  ordtopn1  21490  ordtopn2  21491  leordtval2  21508  icomnfordt  21512  iooordt  21513  perfcls  21661  uncmp  21699  fiuncmp  21700  2ndcdisj2  21753  comppfsc  21828  1stckgenlem  21849  1stckgen  21850  ptbasin  21873  ptbasfi  21877  dfac14lem  21913  dfac14  21914  ptuncnv  22103  ptunhmeo  22104  ptcmpfi  22109  fbun  22136  filconn  22179  isufil2  22204  ufprim  22205  fin1aufil  22228  flimclslem  22280  flimfnfcls  22324  tmdgsum  22391  tsmsgsum  22434  tsmssplit  22447  tsmsxplem1  22448  trust  22525  prdsdsf  22664  prdsmet  22667  prdsbl  22788  cnmpopc  23219  rrxmetlem  23697  rrxmet  23698  rrxdstprj1  23699  ovolctb2  23780  ovolfiniun  23789  finiunmbl  23832  volfiniun  23835  uniioombllem3  23873  uniioombllem4  23874  mbfres2  23933  itg2splitlem  24036  itg2split  24037  itgsplit  24123  limcvallem  24156  ellimc2  24162  limccnp  24176  limccnp2  24177  limcco  24178  dvmptfsum  24259  lhop2  24299  lhop  24300  mdegcl  24350  elply2  24473  elplyd  24479  ply1term  24481  ply0  24485  plyaddlem1  24490  plymullem1  24491  plymullem  24493  mtest  24679  xrlimcnp  25232  jensen  25252  fsumharmonic  25275  chtdif  25421  lgsdir2lem3  25589  lgsquadlem2  25643  dchrisumlem2  25752  dchrisum0lem1b  25777  dchrisum0lem1  25778  pntrlog2bndlem6  25845  pntlemf  25867  shsleji  28834  shsval2i  28851  ssjo  28911  sshhococi  29010  symgcom  30382  gsumle  30490  esumsplit  30925  measun  31083  aean  31116  sxbrsigalem2  31157  bnj970  31831  bnj1137  31877  subfacp1lem2a  32037  subfacp1lem3  32039  subfacp1lem5  32041  erdszelem8  32055  kur14lem7  32069  cvmliftlem10  32151  mrsubvr  32368  frrlem14  32747  noetalem3  32830  refssfne  33317  topjoin  33324  tailf  33334  bj-unrab  33821  bj-2upln1upl  33962  bj-ccinftyssccbar  34079  imadifss  34419  finixpnum  34429  matunitlindflem1  34440  mblfinlem4  34484  prdsbnd  34624  heibor1lem  34640  sspadd2  36504  pclfinN  36588  dochdmj1  38078  mzpcompact2lem  38854  eldioph2  38865  eldioph4b  38914  ttac  39139  pwssplit4  39195  isnumbasgrplem2  39210  isnumbasabl  39212  dfacbasgrp  39214  algsca  39287  algvsca  39288  fiuneneq  39303  rclexi  39481  rtrclex  39483  trclubgNEW  39484  trclexi  39486  rtrclexi  39487  cnvrcl0  39491  cnvtrcl0  39492  dfrtrcl5  39495  trrelsuperrel2dg  39522  dfrcl2  39525  relexp0a  39567  relexpaddss  39569  trclimalb2  39577  frege109d  39608  frege131d  39615  isotone1  39904  grumnudlem  40139  iblsplit  41814  fourierdlem46  42001  sge0resplit  42252  sge0split  42255  sge0splitmpt  42257  sge0xaddlem1  42279  sbgoldbo  43456  gsumsplit2f  43912  setrec1  44296  elpglem2  44316