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

Theorem elssuni 3871
Description: An element of a class is a subclass of its union. Theorem 8.6 of [Quine] p. 54. Also the basis for Proposition 7.20 of [TakeutiZaring] p. 40. (Contributed by NM, 6-Jun-1994.)
Assertion
Ref Expression
elssuni  |-  ( A  e.  B  ->  A  C_ 
U. B )

Proof of Theorem elssuni
StepHypRef Expression
1 ssid 3210 . 2  |-  A  C_  A
2 ssuni 3865 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 651 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1696    C_ wss 3165   U.cuni 3843
This theorem is referenced by:  unissel  3872  ssunieq  3876  pwuni  4222  pwel  4241  uniopel  4286  iunpw  4586  dmrnssfld  4954  unixp0  5222  fvssunirn  5567  sorpssuni  6302  pwuninel2  6315  onfununi  6374  tfrlem9  6417  tfrlem9a  6418  tfrlem13  6422  sbthlem1  6987  sbthlem2  6988  2pwuninel  7032  ordunifi  7123  unifpw  7174  fissuni  7176  dffi3  7200  cantnfp1lem3  7398  oemapvali  7402  cantnflem1  7407  cnfcom3lem  7422  rankuni2b  7541  carduni  7630  r0weon  7656  dfac8clem  7675  cardinfima  7740  alephfp  7751  iunfictbso  7757  dfac5lem4  7769  dfac2a  7772  dfacacn  7783  dfac12lem2  7786  kmlem2  7793  fin23lem16  7977  fin23lem21  7981  isf32lem5  7999  fin1a2lem11  8052  fin1a2lem13  8054  itunitc  8063  axdc2lem  8090  axdc3lem2  8093  ttukeylem5  8156  ttukeylem6  8157  fpwwe2lem11  8278  fpwwe2lem12  8279  fpwwe2lem13  8280  fpwwe2  8281  wunex2  8376  inatsk  8416  tskuni  8421  suplem1pr  8692  suplem2pr  8693  unirnioo  10759  mrcuni  13539  isacs3lem  14285  mrelatlub  14305  dprd2dlem1  15292  lbsextlem2  15928  eltopss  16669  toponss  16683  isbasis3g  16703  baspartn  16708  bastg  16720  tgcl  16723  fctop  16757  cctop  16759  ppttop  16760  epttop  16762  difopn  16787  ssntr  16811  isopn3  16819  isopn3i  16835  toponmre  16846  neiuni  16875  resttopon  16908  restopn2  16924  perfopn  16931  pnfnei  16966  mnfnei  16967  ssidcn  17001  lmcnp  17048  pnrmopn  17087  ist1-2  17091  nrmsep  17101  isnrm2  17102  isnrm3  17103  regsep2  17120  cncmp  17135  hauscmplem  17149  hauscmp  17150  conndisj  17158  cnconn  17164  concompss  17175  islly2  17226  nllyrest  17228  nllyidm  17231  hausllycmp  17236  cldllycmp  17237  lly1stc  17238  kgentopon  17249  kgenss  17254  llycmpkgen2  17261  1stckgen  17265  txuni2  17276  ptpjpre1  17282  ptuni2  17287  ptbasfi  17292  xkouni  17310  txcnpi  17318  ptpjopn  17322  txindis  17344  txnlly  17347  txtube  17350  hausdiag  17355  xkopt  17365  xkococnlem  17369  txcon  17399  qtopuni  17409  qtopkgen  17417  tgqtop  17419  regr1lem  17446  kqreglem1  17448  kqreglem2  17449  kqnrmlem1  17450  kqnrmlem2  17451  hmeoimaf1o  17477  reghmph  17500  nrmhmph  17501  filcon  17594  trfil1  17597  ufildr  17642  flimfil  17680  flimfnfcls  17739  alexsublem  17754  alexsubALTlem3  17759  tgioo  18318  xrtgioo  18328  xrsmopn  18334  opnreen  18352  cnheibor  18469  cnllycmp  18470  lebnumlem1  18475  lebnumlem3  18477  bcthlem5  18766  bcth2  18768  bcth3  18769  voliunlem1  18923  voliunlem3  18925  volsup  18929  opnmbllem  18972  mbfimaopnlem  19026  lhop  19379  ubthlem1  21465  shatomistici  22957  hatomistici  22958  clduni  23304  tpr2rico  23311  hasheuni  23468  prob01  23631  probdsb  23640  totprobd  23644  probmeasb  23648  cndprobtot  23654  orvcelval  23684  pconcon  23777  cvmsf1o  23818  cvmscld  23819  cvmsss2  23820  cvmopnlem  23824  cvmfolem  23825  cvmliftmolem1  23827  cvmliftlem6  23836  cvmliftlem8  23838  cvmlift2lem9  23857  cvmlift2lem11  23859  cvmlift2lem12  23860  cvmlift3lem6  23870  dfon2lem3  24212  dfon2lem7  24216  trpredpred  24302  wfrlem12  24338  wfrlem16  24342  frrlem11  24364  nobndlem2  24418  nobndlem8  24424  nofulllem3  24429  nofulllem5  24431  unint2t  25621  intfmu2  25622  osneisi  25634  ntruni  26348  clsint2  26350  comppfsc  26410  neibastop1  26411  topmeet  26416  topjoin  26417  fnemeet1  26418  fnejoin1  26420  heiborlem1  26638  isnacs3  26888  aomclem4  27257  kelac2  27266  stoweidlem28  27880  stoweidlem50  27902  stoweidlem52  27904  stoweidlem53  27905  stoweidlem54  27906  bnj1450  29396  bnj1501  29413  lssats  29824  dicval  31988  mapdunirnN  32462
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-clab 2283  df-cleq 2289  df-clel 2292  df-nfc 2421  df-v 2803  df-in 3172  df-ss 3179  df-uni 3844
  Copyright terms: Public domain W3C validator