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

Theorem elssuni 3796
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 3139 . 2  |-  A  C_  A
2 ssuni 3790 . 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 3094   U.cuni 3768
This theorem is referenced by:  unissel  3797  ssunieq  3801  pwuni  4144  pwel  4163  uniopel  4207  iunpw  4507  dmrnssfld  4891  unixp0  5158  fvssunirn  5450  sorpssuni  6185  pwuninelALT  6232  onfununi  6291  tfrlem9  6334  tfrlem9a  6335  tfrlem13  6339  sbthlem1  6904  sbthlem2  6905  2pwuninel  6949  ordunifi  7040  unifpw  7091  fissuni  7093  dffi3  7117  cantnfp1lem3  7315  oemapvali  7319  cantnflem1  7324  cnfcom3lem  7339  rankuni2b  7458  carduni  7547  r0weon  7573  dfac8clem  7592  cardinfima  7657  alephfp  7668  iunfictbso  7674  dfac5lem4  7686  dfac2a  7689  dfacacn  7700  dfac12lem2  7703  kmlem2  7710  fin23lem16  7894  fin23lem21  7898  isf32lem5  7916  fin1a2lem11  7969  fin1a2lem13  7971  itunitc  7980  axdc2lem  8007  axdc3lem2  8010  ttukeylem5  8073  ttukeylem6  8074  fpwwe2lem11  8195  fpwwe2lem12  8196  fpwwe2lem13  8197  fpwwe2  8198  wunex2  8293  inatsk  8333  tskuni  8338  suplem1pr  8609  suplem2pr  8610  unirnioo  10674  mrcuni  13450  isacs3lem  14196  mrelatlub  14216  dprd2dlem1  15203  lbsextlem2  15839  eltopss  16580  toponss  16594  isbasis3g  16614  baspartn  16619  bastg  16631  tgcl  16634  fctop  16668  cctop  16670  ppttop  16671  epttop  16673  difopn  16698  ssntr  16722  isopn3  16730  isopn3i  16746  toponmre  16757  neiuni  16786  resttopon  16819  restopn2  16835  perfopn  16842  pnfnei  16877  mnfnei  16878  ssidcn  16912  lmcnp  16959  pnrmopn  16998  ist1-2  17002  nrmsep  17012  isnrm2  17013  isnrm3  17014  regsep2  17031  cncmp  17046  hauscmplem  17060  hauscmp  17061  conndisj  17069  cnconn  17075  concompss  17086  islly2  17137  nllyrest  17139  nllyidm  17142  hausllycmp  17147  cldllycmp  17148  lly1stc  17149  kgentopon  17160  kgenss  17165  llycmpkgen2  17172  1stckgen  17176  txuni2  17187  ptpjpre1  17193  ptuni2  17198  ptbasfi  17203  xkouni  17221  txcnpi  17229  ptpjopn  17233  txindis  17255  txnlly  17258  txtube  17261  hausdiag  17266  xkopt  17276  xkococnlem  17280  txcon  17310  qtopuni  17320  qtopkgen  17328  tgqtop  17330  regr1lem  17357  kqreglem1  17359  kqreglem2  17360  kqnrmlem1  17361  kqnrmlem2  17362  hmeoimaf1o  17388  reghmph  17411  nrmhmph  17412  filcon  17505  trfil1  17508  ufildr  17553  flimfil  17591  flimfnfcls  17650  alexsublem  17665  alexsubALTlem3  17670  tgioo  18229  xrtgioo  18239  xrsmopn  18245  opnreen  18263  cnheibor  18380  cnllycmp  18381  lebnumlem1  18386  lebnumlem3  18388  bcthlem5  18677  bcth2  18679  bcth3  18680  voliunlem1  18834  voliunlem3  18836  volsup  18840  opnmbllem  18883  mbfimaopnlem  18937  lhop  19290  ubthlem1  21374  shatomistici  22866  hatomistici  22867  pconcon  23099  cvmsf1o  23140  cvmscld  23141  cvmsss2  23142  cvmopnlem  23146  cvmfolem  23147  cvmliftmolem1  23149  cvmliftlem6  23158  cvmliftlem8  23160  cvmlift2lem9  23179  cvmlift2lem11  23181  cvmlift2lem12  23182  cvmlift3lem6  23192  dfon2lem3  23475  dfon2lem7  23479  trpredpred  23565  wfrlem12  23601  wfrlem16  23605  frrlem11  23627  axfelem2  23681  axfelem13  23692  axfelem18  23697  axfelem22  23701  unint2t  24850  intfmu2  24851  osneisi  24863  ntruni  25577  clsint2  25579  comppfsc  25639  neibastop1  25640  topmeet  25645  topjoin  25646  fnemeet1  25647  fnejoin1  25649  heiborlem1  25867  isnacs3  26117  aomclem4  26486  kelac2  26495  stoweidlem28  27077  stoweidlem50  27099  stoweidlem52  27101  stoweidlem53  27102  stoweidlem54  27103  bnj1450  28092  bnj1501  28109  lssats  28332  dicval  30496  mapdunirnN  30970
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 2237
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 2243  df-cleq 2249  df-clel 2252  df-nfc 2381  df-v 2742  df-in 3101  df-ss 3108  df-uni 3769
  Copyright terms: Public domain W3C validator