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

Theorem elssuni 4030
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 3354 . 2  |-  A  C_  A
2 ssuni 4024 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 652 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 4    e. wcel 1725    C_ wss 3307   U.cuni 4002
This theorem is referenced by:  unissel  4031  ssunieq  4035  pwuni  4382  pwel  4402  uniopel  4447  iunpw  4745  dmrnssfld  5115  unixp0  5389  fvssunirn  5740  sorpssuni  6517  pwuninel2  6530  onfununi  6589  tfrlem9  6632  tfrlem9a  6633  tfrlem13  6637  sbthlem1  7203  sbthlem2  7204  2pwuninel  7248  ordunifi  7343  unifpw  7395  fissuni  7397  dffi3  7422  cantnfp1lem3  7620  oemapvali  7624  cantnflem1  7629  cnfcom3lem  7644  rankuni2b  7763  carduni  7852  r0weon  7878  dfac8clem  7897  cardinfima  7962  alephfp  7973  iunfictbso  7979  dfac5lem4  7991  dfac2a  7994  dfacacn  8005  dfac12lem2  8008  kmlem2  8015  fin23lem16  8199  fin23lem21  8203  isf32lem5  8221  fin1a2lem11  8274  fin1a2lem13  8276  itunitc  8285  axdc2lem  8312  axdc3lem2  8315  ttukeylem5  8377  ttukeylem6  8378  fpwwe2lem11  8499  fpwwe2lem12  8500  fpwwe2lem13  8501  fpwwe2  8502  wunex2  8597  inatsk  8637  tskuni  8642  suplem1pr  8913  suplem2pr  8914  unirnioo  10988  mrcuni  13829  isacs3lem  14575  mrelatlub  14595  dprd2dlem1  15582  lbsextlem2  16214  eltopss  16963  toponss  16977  isbasis3g  16997  baspartn  17002  bastg  17014  tgcl  17017  fctop  17051  cctop  17053  ppttop  17054  epttop  17056  difopn  17081  ssntr  17105  isopn3  17113  isopn3i  17129  toponmre  17140  neiuni  17169  neiptoptop  17178  resttopon  17208  restopn2  17224  perfopn  17232  pnfnei  17267  mnfnei  17268  ssidcn  17302  lmcnp  17351  pnrmopn  17390  ist1-2  17394  nrmsep  17404  isnrm2  17405  isnrm3  17406  regsep2  17423  cncmp  17438  hauscmplem  17452  hauscmp  17453  conndisj  17462  cnconn  17468  concompss  17479  islly2  17530  nllyrest  17532  nllyidm  17535  hausllycmp  17540  cldllycmp  17541  lly1stc  17542  kgentopon  17553  kgenss  17558  llycmpkgen2  17565  1stckgen  17569  txuni2  17580  ptpjpre1  17586  ptuni2  17591  ptbasfi  17596  xkouni  17614  txcnpi  17623  ptpjopn  17627  txindis  17649  txnlly  17652  txtube  17655  hausdiag  17660  xkopt  17670  xkococnlem  17674  txcon  17704  qtopuni  17717  qtopkgen  17725  tgqtop  17727  regr1lem  17754  kqreglem1  17756  kqreglem2  17757  kqnrmlem1  17758  kqnrmlem2  17759  hmeoimaf1o  17785  reghmph  17808  nrmhmph  17809  filcon  17898  trfil1  17901  ufildr  17946  flimfil  17984  flimfnfcls  18043  alexsublem  18058  alexsubALTlem3  18063  ustbas2  18238  tgioo  18810  xrtgioo  18820  xrsmopn  18826  opnreen  18845  cnheibor  18963  cnllycmp  18964  lebnumlem1  18969  lebnumlem3  18971  bcthlem5  19264  bcth3  19267  voliunlem1  19427  voliunlem3  19429  volsup  19433  opnmbllem  19476  mbfimaopnlem  19530  lhop  19883  ubthlem1  22355  shatomistici  23847  hatomistici  23848  tpr2rico  24293  hasheuni  24458  difelsiga  24499  prob01  24654  probdsb  24663  totprobd  24667  probmeasb  24671  cndprobtot  24677  orvcelval  24709  pconcon  24901  cvmsf1o  24942  cvmscld  24943  cvmsss2  24944  cvmopnlem  24948  cvmfolem  24949  cvmliftmolem1  24951  cvmliftlem6  24960  cvmliftlem8  24962  cvmlift2lem9  24981  cvmlift2lem11  24983  cvmlift2lem12  24984  cvmlift3lem6  24994  dfon2lem3  25391  dfon2lem7  25395  trpredpred  25481  wfrlem12  25517  wfrlem16  25521  frrlem11  25543  nobndlem2  25597  nobndlem8  25603  nofulllem3  25608  nofulllem5  25610  mblfinlem  26185  mbfresfi  26194  ntruni  26262  clsint2  26264  comppfsc  26319  neibastop1  26320  topmeet  26325  topjoin  26326  fnemeet1  26327  fnejoin1  26329  heiborlem1  26452  isnacs3  26696  aomclem4  27064  kelac2  27073  stoweidlem28  27686  stoweidlem50  27708  stoweidlem52  27710  stoweidlem53  27711  stoweidlem54  27712  bnj1450  29171  bnj1501  29188  lssats  29541  dicval  31705  mapdunirnN  32179
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1555  ax-5 1566  ax-17 1626  ax-9 1666  ax-8 1687  ax-6 1744  ax-7 1749  ax-11 1761  ax-12 1950  ax-ext 2411
This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-tru 1328  df-ex 1551  df-nf 1554  df-sb 1659  df-clab 2417  df-cleq 2423  df-clel 2426  df-nfc 2555  df-v 2945  df-in 3314  df-ss 3321  df-uni 4003
  Copyright terms: Public domain W3C validator