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

Theorem ssun2 3738
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 3737 . 2 𝐴 ⊆ (𝐴𝐵)
2 uncom 3718 . 2 (𝐴𝐵) = (𝐵𝐴)
31, 2sseqtri 3599 1 𝐴 ⊆ (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  cun 3537  wss 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2033  ax-13 2233  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-un 3544  df-in 3546  df-ss 3553
This theorem is referenced by:  ssun4  3740  elun2  3742  nsspssun  3818  unv  3922  un00  3962  snsspr2  4285  snsstp3  4288  fvrn0  6111  riotassuni  6525  ovima0  6688  unexb  6833  difex2  6840  rnexg  6967  fnsuppres  7186  brtpos0  7223  wfrlem16  7294  oaabs2  7589  domunsncan  7922  mapunen  7991  ac6sfi  8066  unfir  8090  domunfican  8095  iunfi  8114  elfiun  8196  dffi3  8197  hartogslem1  8307  unwdomg  8349  unxpwdom2  8353  unxpwdom  8354  trcl  8464  unwf  8533  rankunb  8573  r0weon  8695  infxpenlem  8696  alephfplem4  8790  cda1dif  8858  cdainflem  8873  infcda  8890  cfsuc  8939  fin1a2lem10  9091  axdc3lem4  9135  ttukeylem7  9197  fpwwe2lem13  9320  canthp1lem2  9331  gchac  9359  wunrn  9407  wunex2  9416  inar1  9453  ltrelxr  9950  un0mulcl  11174  pnfxr  11781  fzdifsuc  12225  hashbclem  13045  hashf1lem1  13048  ccatrn  13171  trclublem  13528  relexprng  13580  fsumsplit  14264  o1fsum  14332  incexclem  14353  fprodsplit  14481  vdwlem5  15473  vdwlem8  15476  ramcl2  15504  srnginvl  15781  lmodvsca  15790  ipssca  15797  ipsvsca  15798  ipsip  15799  phlvsca  15807  phlip  15808  odrngtset  15839  odrngle  15840  odrngds  15841  prdssca  15885  prdsvsca  15889  prdsip  15890  prdsle  15891  prdsds  15893  prdstset  15895  prdshom  15896  prdsco  15897  imasds  15942  imassca  15948  imasvsca  15949  imasip  15950  imastset  15951  imasle  15952  mreexexlemd  16073  mreexexlem2d  16074  mreexexlem3d  16075  drsdirfi  16707  ipolerval  16925  psdmrn  16976  dirge  17006  gsumzsplit  18096  gsumsplit2  18098  gsumzunsnd  18124  gsum2dlem2  18139  dprdfadd  18188  dmdprdsplit2lem  18213  dmdprdsplit2  18214  dmdprdsplit  18215  dprdsplit  18216  ablfac1eulem  18240  pgpfaclem1  18249  lspun  18754  lbsextlem2  18926  lbsextlem3  18927  lbsextlem4  18928  psrbagaddcl  19137  psrsca  19156  psrvscafval  19157  mplsubglem  19201  mplcoe5  19235  opsrtoslem2  19252  cnfldcj  19520  cnfldtset  19521  cnfldle  19522  cnfldds  19523  cnfldunif  19524  ordtbas2  20747  ordtbas  20748  ordtopn1  20750  ordtopn2  20751  leordtval2  20768  icomnfordt  20772  iooordt  20773  perfcls  20921  uncmp  20958  fiuncmp  20959  2ndcdisj2  21012  comppfsc  21087  1stckgenlem  21108  1stckgen  21109  ptbasin  21132  ptbasfi  21136  dfac14lem  21172  dfac14  21173  ptuncnv  21362  ptunhmeo  21363  ptcmpfi  21368  fbun  21396  filcon  21439  isufil2  21464  ufprim  21465  fin1aufil  21488  flimclslem  21540  flimfnfcls  21584  tmdgsum  21651  tsmsgsum  21694  tsmssplit  21707  tsmsxplem1  21708  trust  21785  prdsdsf  21923  prdsmet  21926  prdsbl  22047  cnmpt2pc  22466  rrxmetlem  22915  rrxmet  22916  rrxdstprj1  22917  ovolctb2  22984  ovolfiniun  22993  finiunmbl  23036  volfiniun  23039  uniioombllem3  23076  uniioombllem4  23077  mbfres2  23135  itg2splitlem  23238  itg2split  23239  itgsplit  23325  limcvallem  23358  ellimc2  23364  limccnp  23378  limccnp2  23379  limcco  23380  dvmptfsum  23459  lhop2  23499  lhop  23500  mdegcl  23550  elply2  23673  elplyd  23679  ply1term  23681  ply0  23685  plyaddlem1  23690  plymullem1  23691  plymullem  23693  mtest  23879  xrlimcnp  24412  jensen  24432  fsumharmonic  24455  chtdif  24601  lgsdir2lem3  24769  lgsquadlem2  24823  dchrisumlem2  24896  dchrisum0lem1b  24921  dchrisum0lem1  24922  pntrlog2bndlem6  24989  pntlemf  25011  eupap1  26269  shsleji  27419  shsval2i  27436  ssjo  27496  sshhococi  27595  gsumle  28916  esumsplit  29248  measun  29407  aean  29440  sxbrsigalem2  29481  bnj970  30077  bnj1137  30123  subfacp1lem2a  30222  subfacp1lem3  30224  subfacp1lem5  30226  erdszelem8  30240  kur14lem7  30254  cvmliftlem10  30336  mrsubvr  30468  nofulllem4  30910  refssfne  31329  topjoin  31336  tailf  31346  bj-unrab  31910  bj-2upln1upl  32001  bj-ccinftyssccbar  32078  imadifss  32350  finixpnum  32360  matunitlindflem1  32371  mblfinlem4  32415  prdsbnd  32558  heibor1lem  32574  sspadd2  33916  pclfinN  34000  dochdmj1  35493  mzpcompact2lem  36128  eldioph2  36139  eldioph4b  36189  ttac  36417  pwssplit4  36473  isnumbasgrplem2  36489  isnumbasabl  36491  dfacbasgrp  36493  algsca  36566  algvsca  36567  fiuneneq  36590  rclexi  36737  rtrclex  36739  trclubgNEW  36740  trclexi  36742  rtrclexi  36743  cnvrcl0  36747  cnvtrcl0  36748  dfrtrcl5  36751  trrelsuperrel2dg  36778  dfrcl2  36781  relexp0a  36823  relexpaddss  36825  trclimalb2  36833  frege109d  36864  frege131d  36871  isotone1  37162  iblsplit  38655  fourierdlem46  38842  sge0resplit  39096  sge0split  39099  sge0splitmpt  39101  sge0xaddlem1  39123  gsumsplit2f  41931
  Copyright terms: Public domain W3C validator