MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ssun2 Structured version   Visualization version   Unicode version

Theorem ssun2 3589
Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
ssun2  |-  A  C_  ( B  u.  A
)

Proof of Theorem ssun2
StepHypRef Expression
1 ssun1 3588 . 2  |-  A  C_  ( A  u.  B
)
2 uncom 3569 . 2  |-  ( A  u.  B )  =  ( B  u.  A
)
31, 2sseqtri 3450 1  |-  A  C_  ( B  u.  A
)
Colors of variables: wff setvar class
Syntax hints:    u. cun 3388    C_ wss 3390
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1677  ax-4 1690  ax-5 1766  ax-6 1813  ax-7 1859  ax-10 1932  ax-11 1937  ax-12 1950  ax-13 2104  ax-ext 2451
This theorem depends on definitions:  df-bi 190  df-or 377  df-an 378  df-tru 1455  df-ex 1672  df-nf 1676  df-sb 1806  df-clab 2458  df-cleq 2464  df-clel 2467  df-nfc 2601  df-v 3033  df-un 3395  df-in 3397  df-ss 3404
This theorem is referenced by:  ssun4  3591  elun2  3593  nsspssun  3667  unv  3765  un00  3804  snsspr2  4113  snsstp3  4116  fvrn0  5901  riotassuni  6306  ovima0  6467  unexb  6610  difex2  6617  rnexg  6744  fnsuppres  6961  brtpos0  6998  wfrlem16  7069  oaabs2  7364  domunsncan  7690  mapunen  7759  ac6sfi  7833  unfir  7857  domunfican  7862  iunfi  7880  elfiun  7962  dffi3  7963  hartogslem1  8075  unwdomg  8117  unxpwdom2  8121  unxpwdom  8122  trcl  8230  unwf  8299  rankunb  8339  r0weon  8461  infxpenlem  8462  alephfplem4  8556  cda1dif  8624  cdainflem  8639  infcda  8656  cfsuc  8705  fin1a2lem10  8857  axdc3lem4  8901  ttukeylem7  8963  fpwwe2lem13  9085  canthp1lem2  9096  gchac  9124  wunrn  9172  wunex2  9181  inar1  9218  ltrelxr  9713  un0mulcl  10928  pnfxr  11435  fzdifsuc  11881  hashbclem  12656  hashf1lem1  12659  ccatfnOLD  12769  ccatrn  12784  trclublem  13134  relexprng  13186  fsumsplit  13883  o1fsum  13950  incexclem  13971  fprodsplit  14097  vdwlem5  15014  vdwlem8  15017  ramcl2  15052  ramcl2OLD  15053  srnginvl  15334  lmodvsca  15343  ipssca  15350  ipsvsca  15351  ipsip  15352  phlvsca  15360  phlip  15361  odrngtset  15386  odrngle  15387  odrngds  15388  prdssca  15432  prdsvsca  15436  prdsip  15437  prdsle  15438  prdsds  15440  prdstset  15442  prdshom  15443  prdsco  15444  imasds  15492  imassca  15498  imasvsca  15499  imasip  15500  imastset  15501  imasle  15502  imasdsOLD  15504  mreexexlemd  15628  mreexexlem2d  15629  mreexexlem3d  15630  drsdirfi  16261  ipolerval  16480  psdmrn  16531  dirge  16561  gsumzsplit  17638  gsumsplit2  17640  gsumzunsnd  17666  gsum2dlem2  17681  dprdfadd  17731  dmdprdsplit2lem  17756  dmdprdsplit2  17757  dmdprdsplit  17758  dprdsplit  17759  ablfac1eulem  17783  pgpfaclem1  17792  lspun  18288  lbsextlem2  18460  lbsextlem3  18461  lbsextlem4  18462  psrbagaddcl  18671  psrsca  18690  psrvscafval  18691  mplsubglem  18735  mplcoe5  18769  opsrtoslem2  18785  cnfldcj  19054  cnfldtset  19055  cnfldle  19056  cnfldds  19057  cnfldunif  19058  ordtbas2  20284  ordtbas  20285  ordtopn1  20287  ordtopn2  20288  leordtval2  20305  icomnfordt  20309  iooordt  20310  perfcls  20458  uncmp  20495  fiuncmp  20496  2ndcdisj2  20549  comppfsc  20624  1stckgenlem  20645  1stckgen  20646  ptbasin  20669  ptbasfi  20673  dfac14lem  20709  dfac14  20710  ptuncnv  20899  ptunhmeo  20900  ptcmpfi  20905  fbun  20933  filcon  20976  isufil2  21001  ufprim  21002  fin1aufil  21025  flimclslem  21077  flimfnfcls  21121  tmdgsum  21188  tsmsgsum  21231  tsmssplit  21244  tsmsxplem1  21245  trust  21322  prdsdsf  21460  prdsmet  21463  prdsbl  21584  cnmpt2pc  22034  rrxmetlem  22439  rrxmet  22440  rrxdstprj1  22441  ovolctb2  22523  ovolfiniun  22532  finiunmbl  22576  volfiniun  22579  uniioombllem3  22622  uniioombllem4  22623  mbfres2  22680  itg2splitlem  22785  itg2split  22786  itgsplit  22872  limcvallem  22905  ellimc2  22911  limccnp  22925  limccnp2  22926  limcco  22927  dvmptfsum  23006  lhop2  23046  lhop  23047  mdegcl  23097  elply2  23229  elplyd  23235  ply1term  23237  ply0  23241  plyaddlem1  23246  plymullem1  23247  plymullem  23249  mtest  23438  xrlimcnp  23973  jensen  23993  fsumharmonic  24016  chtdif  24164  lgsdir2lem3  24332  lgsquadlem2  24362  dchrisumlem2  24407  dchrisum0lem1b  24432  dchrisum0lem1  24433  pntrlog2bndlem6  24500  pntlemf  24522  eupap1  25783  shsleji  27104  shsval2i  27121  ssjo  27181  sshhococi  27280  gsumle  28616  esumsplit  28948  measun  29107  aean  29140  sxbrsigalem2  29181  bnj970  29830  bnj1137  29876  subfacp1lem2a  29975  subfacp1lem3  29977  subfacp1lem5  29979  erdszelem8  29993  kur14lem7  30007  cvmliftlem10  30089  mrsubvr  30221  nofulllem4  30665  refssfne  31085  topjoin  31092  tailf  31102  bj-unrab  31597  bj-2upln1upl  31688  bj-ccinftyssccbar  31730  imadifss  31992  finixpnum  31994  mblfinlem4  32044  prdsbnd  32189  heibor1lem  32205  sspadd2  33452  pclfinN  33536  dochdmj1  35029  mzpcompact2lem  35664  eldioph2  35675  eldioph4b  35725  ttac  35962  pwssplit4  36018  isnumbasgrplem2  36034  isnumbasabl  36036  dfacbasgrp  36038  algsca  36118  algvsca  36119  fiuneneq  36142  rclexi  36293  rtrclex  36295  trclubgNEW  36296  trclexi  36298  rtrclexi  36299  cnvrcl0  36303  cnvtrcl0  36304  dfrtrcl5  36307  trrelsuperrel2dg  36334  dfrcl2  36337  relexp0a  36379  relexpaddss  36381  trclimalb2  36389  frege109d  36420  frege131d  36427  iblsplit  37940  fourierdlem46  38128  sge0resplit  38362  sge0split  38365  sge0splitmpt  38367  sge0xaddlem1  38389  gsumsplit2f  40654
  Copyright terms: Public domain W3C validator