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

Theorem ssun2 3976
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 3975 . 2 𝐴 ⊆ (𝐴𝐵)
2 uncom 3956 . 2 (𝐴𝐵) = (𝐵𝐴)
31, 2sseqtri 3834 1 𝐴 ⊆ (𝐵𝐴)
Colors of variables: wff setvar class
Syntax hints:  cun 3767  wss 3769
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2068  ax-7 2104  ax-9 2165  ax-10 2185  ax-11 2201  ax-12 2214  ax-13 2420  ax-ext 2784
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2061  df-clab 2793  df-cleq 2799  df-clel 2802  df-nfc 2937  df-v 3393  df-un 3774  df-in 3776  df-ss 3783
This theorem is referenced by:  ssun4  3978  elun2  3980  nsspssun  4059  unv  4169  un00  4209  snsspr2  4536  snsstp3  4539  fvrn0  6436  riotassuni  6872  ovima0  7043  unexb  7188  difex2  7199  rnexg  7328  fnsuppres  7557  brtpos0  7594  wfrlem16  7666  oaabs2  7962  domunsncan  8299  mapunen  8368  ac6sfi  8443  unfir  8467  domunfican  8472  iunfi  8493  elfiun  8575  dffi3  8576  hartogslem1  8686  unwdomg  8728  unxpwdom2  8732  unxpwdom  8733  trcl  8851  unwf  8920  rankunb  8960  r0weon  9118  infxpenlem  9119  alephfplem4  9213  cda1dif  9283  cdainflem  9298  infcda  9315  cfsuc  9364  fin1a2lem10  9516  axdc3lem4  9560  ttukeylem7  9622  fpwwe2lem13  9749  canthp1lem2  9760  gchac  9788  wunrn  9836  wunex2  9845  inar1  9882  pnfxr  10377  ltrelxr  10384  un0mulcl  11593  fzdifsuc  12623  hashbclem  13453  hashf1lem1  13456  ccatrn  13586  trclublem  13959  relexprng  14009  fsumsplit  14694  o1fsum  14767  incexclem  14790  fprodsplit  14917  vdwlem5  15906  vdwlem8  15909  ramcl2  15937  srnginvl  16223  lmodvsca  16232  ipssca  16239  ipsvsca  16240  ipsip  16241  phlvsca  16249  phlip  16250  odrngtset  16275  odrngle  16276  odrngds  16277  prdssca  16321  prdsvsca  16325  prdsip  16326  prdsle  16327  prdsds  16329  prdstset  16331  prdshom  16332  prdsco  16333  imasds  16378  imassca  16384  imasvsca  16385  imasip  16386  imastset  16387  imasle  16388  mreexexlemd  16509  mreexexlem2d  16510  mreexexlem3d  16511  drsdirfi  17143  ipolerval  17361  psdmrn  17412  dirge  17442  gsumzsplit  18528  gsumsplit2  18530  gsumzunsnd  18556  gsum2dlem2  18571  dprdfadd  18621  dmdprdsplit2lem  18646  dmdprdsplit2  18647  dmdprdsplit  18648  dprdsplit  18649  ablfac1eulem  18673  pgpfaclem1  18682  lspun  19194  lbsextlem2  19368  lbsextlem3  19369  lbsextlem4  19370  psrbagaddcl  19579  psrsca  19598  psrvscafval  19599  mplsubglem  19643  mplcoe5  19677  opsrtoslem2  19693  cnfldcj  19961  cnfldtset  19962  cnfldle  19963  cnfldds  19964  cnfldunif  19965  ordtbas2  21209  ordtbas  21210  ordtopn1  21212  ordtopn2  21213  leordtval2  21230  icomnfordt  21234  iooordt  21235  perfcls  21383  uncmp  21420  fiuncmp  21421  2ndcdisj2  21474  comppfsc  21549  1stckgenlem  21570  1stckgen  21571  ptbasin  21594  ptbasfi  21598  dfac14lem  21634  dfac14  21635  ptuncnv  21824  ptunhmeo  21825  ptcmpfi  21830  fbun  21857  filconn  21900  isufil2  21925  ufprim  21926  fin1aufil  21949  flimclslem  22001  flimfnfcls  22045  tmdgsum  22112  tsmsgsum  22155  tsmssplit  22168  tsmsxplem1  22169  trust  22246  prdsdsf  22385  prdsmet  22388  prdsbl  22509  cnmpt2pc  22940  rrxmetlem  23402  rrxmet  23403  rrxdstprj1  23404  ovolctb2  23473  ovolfiniun  23482  finiunmbl  23525  volfiniun  23528  uniioombllem3  23566  uniioombllem4  23567  mbfres2  23626  itg2splitlem  23729  itg2split  23730  itgsplit  23816  limcvallem  23849  ellimc2  23855  limccnp  23869  limccnp2  23870  limcco  23871  dvmptfsum  23952  lhop2  23992  lhop  23993  mdegcl  24043  elply2  24166  elplyd  24172  ply1term  24174  ply0  24178  plyaddlem1  24183  plymullem1  24184  plymullem  24186  mtest  24372  xrlimcnp  24909  jensen  24929  fsumharmonic  24952  chtdif  25098  lgsdir2lem3  25266  lgsquadlem2  25320  dchrisumlem2  25393  dchrisum0lem1b  25418  dchrisum0lem1  25419  pntrlog2bndlem6  25486  pntlemf  25508  shsleji  28557  shsval2i  28574  ssjo  28634  sshhococi  28733  gsumle  30104  esumsplit  30440  measun  30599  aean  30632  sxbrsigalem2  30673  bnj970  31340  bnj1137  31386  subfacp1lem2a  31485  subfacp1lem3  31487  subfacp1lem5  31489  erdszelem8  31503  kur14lem7  31517  cvmliftlem10  31599  mrsubvr  31731  noetalem3  32186  refssfne  32674  topjoin  32681  tailf  32691  bj-unrab  33233  bj-2upln1upl  33322  bj-ccinftyssccbar  33422  imadifss  33697  finixpnum  33707  matunitlindflem1  33718  mblfinlem4  33762  prdsbnd  33903  heibor1lem  33919  sspadd2  35596  pclfinN  35680  dochdmj1  37171  mzpcompact2lem  37816  eldioph2  37827  eldioph4b  37877  ttac  38104  pwssplit4  38160  isnumbasgrplem2  38175  isnumbasabl  38177  dfacbasgrp  38179  algsca  38252  algvsca  38253  fiuneneq  38276  rclexi  38422  rtrclex  38424  trclubgNEW  38425  trclexi  38427  rtrclexi  38428  cnvrcl0  38432  cnvtrcl0  38433  dfrtrcl5  38436  trrelsuperrel2dg  38463  dfrcl2  38466  relexp0a  38508  relexpaddss  38510  trclimalb2  38518  frege109d  38549  frege131d  38556  isotone1  38846  iblsplit  40661  fourierdlem46  40848  sge0resplit  41102  sge0split  41105  sge0splitmpt  41107  sge0xaddlem1  41129  sbgoldbo  42250  gsumsplit2f  42711  setrec1  43006  elpglem2  43026
  Copyright terms: Public domain W3C validator