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

Theorem elssuni 3829
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 3172 . 2  |-  A  C_  A
2 ssuni 3823 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 654 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621    C_ wss 3127   U.cuni 3801
This theorem is referenced by:  unissel  3830  ssunieq  3834  pwuni  4178  pwel  4197  uniopel  4242  iunpw  4542  dmrnssfld  4926  unixp0  5193  fvssunirn  5485  sorpssuni  6220  pwuninelALT  6267  onfununi  6326  tfrlem9  6369  tfrlem9a  6370  tfrlem13  6374  sbthlem1  6939  sbthlem2  6940  2pwuninel  6984  ordunifi  7075  unifpw  7126  fissuni  7128  dffi3  7152  cantnfp1lem3  7350  oemapvali  7354  cantnflem1  7359  cnfcom3lem  7374  rankuni2b  7493  carduni  7582  r0weon  7608  dfac8clem  7627  cardinfima  7692  alephfp  7703  iunfictbso  7709  dfac5lem4  7721  dfac2a  7724  dfacacn  7735  dfac12lem2  7738  kmlem2  7745  fin23lem16  7929  fin23lem21  7933  isf32lem5  7951  fin1a2lem11  8004  fin1a2lem13  8006  itunitc  8015  axdc2lem  8042  axdc3lem2  8045  ttukeylem5  8108  ttukeylem6  8109  fpwwe2lem11  8230  fpwwe2lem12  8231  fpwwe2lem13  8232  fpwwe2  8233  wunex2  8328  inatsk  8368  tskuni  8373  suplem1pr  8644  suplem2pr  8645  unirnioo  10709  mrcuni  13485  isacs3lem  14231  mrelatlub  14251  dprd2dlem1  15238  lbsextlem2  15874  eltopss  16615  toponss  16629  isbasis3g  16649  baspartn  16654  bastg  16666  tgcl  16669  fctop  16703  cctop  16705  ppttop  16706  epttop  16708  difopn  16733  ssntr  16757  isopn3  16765  isopn3i  16781  toponmre  16792  neiuni  16821  resttopon  16854  restopn2  16870  perfopn  16877  pnfnei  16912  mnfnei  16913  ssidcn  16947  lmcnp  16994  pnrmopn  17033  ist1-2  17037  nrmsep  17047  isnrm2  17048  isnrm3  17049  regsep2  17066  cncmp  17081  hauscmplem  17095  hauscmp  17096  conndisj  17104  cnconn  17110  concompss  17121  islly2  17172  nllyrest  17174  nllyidm  17177  hausllycmp  17182  cldllycmp  17183  lly1stc  17184  kgentopon  17195  kgenss  17200  llycmpkgen2  17207  1stckgen  17211  txuni2  17222  ptpjpre1  17228  ptuni2  17233  ptbasfi  17238  xkouni  17256  txcnpi  17264  ptpjopn  17268  txindis  17290  txnlly  17293  txtube  17296  hausdiag  17301  xkopt  17311  xkococnlem  17315  txcon  17345  qtopuni  17355  qtopkgen  17363  tgqtop  17365  regr1lem  17392  kqreglem1  17394  kqreglem2  17395  kqnrmlem1  17396  kqnrmlem2  17397  hmeoimaf1o  17423  reghmph  17446  nrmhmph  17447  filcon  17540  trfil1  17543  ufildr  17588  flimfil  17626  flimfnfcls  17685  alexsublem  17700  alexsubALTlem3  17705  tgioo  18264  xrtgioo  18274  xrsmopn  18280  opnreen  18298  cnheibor  18415  cnllycmp  18416  lebnumlem1  18421  lebnumlem3  18423  bcthlem5  18712  bcth2  18714  bcth3  18715  voliunlem1  18869  voliunlem3  18871  volsup  18875  opnmbllem  18918  mbfimaopnlem  18972  lhop  19325  ubthlem1  21409  shatomistici  22901  hatomistici  22902  pconcon  23134  cvmsf1o  23175  cvmscld  23176  cvmsss2  23177  cvmopnlem  23181  cvmfolem  23182  cvmliftmolem1  23184  cvmliftlem6  23193  cvmliftlem8  23195  cvmlift2lem9  23214  cvmlift2lem11  23216  cvmlift2lem12  23217  cvmlift3lem6  23227  dfon2lem3  23510  dfon2lem7  23514  trpredpred  23600  wfrlem12  23636  wfrlem16  23640  frrlem11  23662  axfelem2  23716  axfelem13  23727  axfelem18  23732  axfelem22  23736  unint2t  24885  intfmu2  24886  osneisi  24898  ntruni  25612  clsint2  25614  comppfsc  25674  neibastop1  25675  topmeet  25680  topjoin  25681  fnemeet1  25682  fnejoin1  25684  heiborlem1  25902  isnacs3  26152  aomclem4  26521  kelac2  26530  stoweidlem28  27112  stoweidlem50  27134  stoweidlem52  27136  stoweidlem53  27137  stoweidlem54  27138  bnj1450  28129  bnj1501  28146  lssats  28369  dicval  30533  mapdunirnN  31007
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1927  ax-ext 2239
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1884  df-clab 2245  df-cleq 2251  df-clel 2254  df-nfc 2383  df-v 2765  df-in 3134  df-ss 3141  df-uni 3802
  Copyright terms: Public domain W3C validator