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

Theorem ssun2 4132
Description: Subclass relationship for union of classes. (Contributed by NM, 30-Aug-1993.)
Assertion
Ref Expression
ssun2 𝐴 ⊆ (𝐵𝐴)

Proof of Theorem ssun2
StepHypRef Expression
1 ssun1 4131 . 2 𝐴 ⊆ (𝐴𝐵)
2 uncom 4112 . 2 (𝐴𝐵) = (𝐵𝐴)
31, 2sseqtri 3979 1 𝐴 ⊆ (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  cun 3907  wss 3909
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 2709
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 2716  df-cleq 2730  df-clel 2816  df-v 3446  df-un 3914  df-in 3916  df-ss 3926
This theorem is referenced by:  ssun4  4134  elun2  4136  nsspssun  4216  unv  4354  un00  4401  pwunss  4577  snsspr2  4774  snsstp3  4777  fvrn0  6870  riotassuni  7349  ovima0  7528  unexb  7675  difex2  7687  rnexg  7834  xpord2indlem  8072  xpord3inddlem  8079  fnsuppres  8115  brtpos0  8157  frrlem14  8223  wfrlem16OLD  8263  oaabs2  8588  domunsncan  8975  mapunen  9049  ac6sfi  9190  unfir  9217  domunfican  9223  iunfi  9243  elfiun  9325  dffi3  9326  hartogslem1  9437  unwdomg  9479  unxpwdom2  9483  unxpwdom  9484  trcl  9623  unwf  9705  rankunb  9745  r0weon  9907  infxpenlem  9908  alephfplem4  10002  dju1dif  10067  cdainflem  10082  infdju  10103  cfsuc  10152  fin1a2lem10  10304  axdc3lem4  10348  ttukeylem7  10410  fpwwe2lem12  10537  canthp1lem2  10548  gchac  10576  wunrn  10624  wunex2  10633  inar1  10670  pnfxr  11168  ltrelxr  11175  un0mulcl  12406  fzdifsuc  13456  seqexw  13877  hashbclem  14303  hashf1lem1  14307  hashf1lem1OLD  14308  ccatrn  14431  trclublem  14840  relexprng  14891  fsumsplit  15586  o1fsum  15658  incexclem  15681  fprodsplit  15809  vdwlem5  16817  vdwlem8  16820  ramcl2  16848  srnginvl  17154  lmodvsca  17170  ipssca  17181  ipsvsca  17182  ipsip  17183  phlvsca  17191  phlip  17192  odrngtset  17248  odrngle  17249  odrngds  17250  prdssca  17298  prdsvsca  17302  prdsip  17303  prdsle  17304  prdsds  17306  prdstset  17308  prdshom  17309  prdsco  17310  imasds  17355  imassca  17361  imasvsca  17362  imasip  17363  imastset  17364  imasle  17365  mreexexlemd  17484  mreexexlem2d  17485  mreexexlem3d  17486  drsdirfi  18154  ipolerval  18381  psdmrn  18422  dirge  18452  grpinvfval  18749  mulgfval  18833  gsumzsplit  19663  gsumsplit2  19665  gsumzunsnd  19692  gsum2dlem2  19707  dprdfadd  19758  dmdprdsplit2lem  19783  dmdprdsplit2  19784  dmdprdsplit  19785  dprdsplit  19786  ablfac1eulem  19810  pgpfaclem1  19819  lspun  20401  lbsextlem2  20573  lbsextlem3  20574  lbsextlem4  20575  cnfldcj  20756  cnfldtset  20757  cnfldle  20758  cnfldds  20759  cnfldunif  20760  psrbagaddclOLD  21284  psrsca  21310  psrvscafval  21311  mplsubglem  21357  mplcoe5  21393  opsrtoslem2  21415  ordtbas2  22494  ordtbas  22495  ordtopn1  22497  ordtopn2  22498  leordtval2  22515  icomnfordt  22519  iooordt  22520  perfcls  22668  uncmp  22706  fiuncmp  22707  2ndcdisj2  22760  comppfsc  22835  1stckgenlem  22856  1stckgen  22857  ptbasin  22880  ptbasfi  22884  dfac14lem  22920  dfac14  22921  ptuncnv  23110  ptunhmeo  23111  ptcmpfi  23116  fbun  23143  filconn  23186  isufil2  23211  ufprim  23212  fin1aufil  23235  flimclslem  23287  flimfnfcls  23331  tmdgsum  23398  tsmsgsum  23442  tsmssplit  23455  tsmsxplem1  23456  trust  23533  prdsdsf  23672  prdsmet  23675  prdsbl  23799  cnmpopc  24243  rrxmetlem  24723  rrxmet  24724  rrxdstprj1  24725  ovolctb2  24808  ovolfiniun  24817  finiunmbl  24860  volfiniun  24863  uniioombllem3  24901  uniioombllem4  24902  mbfres2  24961  itg2splitlem  25065  itg2split  25066  itgsplit  25152  limcvallem  25187  ellimc2  25193  limccnp  25207  limccnp2  25208  limcco  25209  dvmptfsum  25291  lhop2  25331  lhop  25332  mdegcl  25386  elply2  25509  elplyd  25515  ply1term  25517  ply0  25521  plyaddlem1  25526  plymullem1  25527  plymullem  25529  mtest  25715  xrlimcnp  26270  jensen  26290  fsumharmonic  26313  chtdif  26459  lgsdir2lem3  26627  lgsquadlem2  26681  dchrisumlem2  26790  dchrisum0lem1b  26815  dchrisum0lem1  26816  pntrlog2bndlem6  26883  pntlemf  26905  nosupinfsep  27032  noetasuplem4  27036  noetalem1  27041  cofcutrtime  27195  shsleji  30141  shsval2i  30158  ssjo  30218  sshhococi  30317  gsumle  31757  symgcom  31759  idlsrgtset  32070  esumsplit  32456  measun  32614  aean  32647  sxbrsigalem2  32690  bnj970  33363  bnj1137  33411  subfacp1lem2a  33578  subfacp1lem3  33580  subfacp1lem5  33582  erdszelem8  33596  kur14lem7  33610  cvmliftlem10  33692  mrsubvr  33909  addsunif  34301  negsval  34313  refssfne  34762  topjoin  34769  tailf  34779  bj-unrab  35328  bj-2upln1upl  35427  bj-ccinftyssccbar  35621  imadifss  35985  finixpnum  35995  matunitlindflem1  36006  mblfinlem4  36050  prdsbnd  36184  heibor1lem  36200  sspadd2  38211  pclfinN  38295  dochdmj1  39785  mzpcompact2lem  40977  eldioph2  40988  eldioph4b  41037  ttac  41263  pwssplit4  41319  isnumbasgrplem2  41334  isnumbasabl  41336  dfacbasgrp  41338  algsca  41411  algvsca  41412  fiuneneq  41427  rclexi  41792  rtrclex  41794  trclubgNEW  41795  trclexi  41797  rtrclexi  41798  cnvrcl0  41802  cnvtrcl0  41803  dfrtrcl5  41806  trrelsuperrel2dg  41848  dfrcl2  41851  relexp0a  41893  relexpaddss  41895  trclimalb2  41903  frege109d  41934  frege131d  41941  isotone1  42225  grumnudlem  42470  iblsplit  44102  fourierdlem46  44288  sge0resplit  44542  sge0split  44545  sge0splitmpt  44547  sge0xaddlem1  44569  sbgoldbo  45874  gsumsplit2f  46009  setrec1  47031  elpglem2  47052
  Copyright terms: Public domain W3C validator