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

Theorem elssuni 4043
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 3367 . 2  |-  A  C_  A
2 ssuni 4037 . 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 3320   U.cuni 4015
This theorem is referenced by:  unissel  4044  ssunieq  4048  pwuni  4395  pwel  4415  uniopel  4460  iunpw  4759  dmrnssfld  5129  unixp0  5403  fvssunirn  5754  sorpssuni  6531  pwuninel2  6544  onfununi  6603  tfrlem9  6646  tfrlem9a  6647  tfrlem13  6651  sbthlem1  7217  sbthlem2  7218  2pwuninel  7262  ordunifi  7357  unifpw  7409  fissuni  7411  dffi3  7436  cantnfp1lem3  7636  oemapvali  7640  cantnflem1  7645  cnfcom3lem  7660  rankuni2b  7779  carduni  7868  r0weon  7894  dfac8clem  7913  cardinfima  7978  alephfp  7989  iunfictbso  7995  dfac5lem4  8007  dfac2a  8010  dfacacn  8021  dfac12lem2  8024  kmlem2  8031  fin23lem16  8215  fin23lem21  8219  isf32lem5  8237  fin1a2lem11  8290  fin1a2lem13  8292  itunitc  8301  axdc2lem  8328  axdc3lem2  8331  ttukeylem5  8393  ttukeylem6  8394  fpwwe2lem11  8515  fpwwe2lem12  8516  fpwwe2lem13  8517  fpwwe2  8518  wunex2  8613  inatsk  8653  tskuni  8658  suplem1pr  8929  suplem2pr  8930  unirnioo  11004  mrcuni  13846  isacs3lem  14592  mrelatlub  14612  dprd2dlem1  15599  lbsextlem2  16231  eltopss  16980  toponss  16994  isbasis3g  17014  baspartn  17019  bastg  17031  tgcl  17034  fctop  17068  cctop  17070  ppttop  17071  epttop  17073  difopn  17098  ssntr  17122  isopn3  17130  isopn3i  17146  toponmre  17157  neiuni  17186  neiptoptop  17195  resttopon  17225  restopn2  17241  perfopn  17249  pnfnei  17284  mnfnei  17285  ssidcn  17319  lmcnp  17368  pnrmopn  17407  ist1-2  17411  nrmsep  17421  isnrm2  17422  isnrm3  17423  regsep2  17440  cncmp  17455  hauscmplem  17469  hauscmp  17470  conndisj  17479  cnconn  17485  concompss  17496  islly2  17547  nllyrest  17549  nllyidm  17552  hausllycmp  17557  cldllycmp  17558  lly1stc  17559  kgentopon  17570  kgenss  17575  llycmpkgen2  17582  1stckgen  17586  txuni2  17597  ptpjpre1  17603  ptuni2  17608  ptbasfi  17613  xkouni  17631  txcnpi  17640  ptpjopn  17644  txindis  17666  txnlly  17669  txtube  17672  hausdiag  17677  xkopt  17687  xkococnlem  17691  txcon  17721  qtopuni  17734  qtopkgen  17742  tgqtop  17744  regr1lem  17771  kqreglem1  17773  kqreglem2  17774  kqnrmlem1  17775  kqnrmlem2  17776  hmeoimaf1o  17802  reghmph  17825  nrmhmph  17826  filcon  17915  trfil1  17918  ufildr  17963  flimfil  18001  flimfnfcls  18060  alexsublem  18075  alexsubALTlem3  18080  ustbas2  18255  tgioo  18827  xrtgioo  18837  xrsmopn  18843  opnreen  18862  cnheibor  18980  cnllycmp  18981  lebnumlem1  18986  lebnumlem3  18988  bcthlem5  19281  bcth3  19284  voliunlem1  19444  voliunlem3  19446  volsup  19450  opnmbllem  19493  mbfimaopnlem  19547  lhop  19900  ubthlem1  22372  shatomistici  23864  hatomistici  23865  tpr2rico  24310  hasheuni  24475  difelsiga  24516  prob01  24671  probdsb  24680  totprobd  24684  probmeasb  24688  cndprobtot  24694  orvcelval  24726  pconcon  24918  cvmsf1o  24959  cvmscld  24960  cvmsss2  24961  cvmopnlem  24965  cvmfolem  24966  cvmliftmolem1  24968  cvmliftlem6  24977  cvmliftlem8  24979  cvmlift2lem9  24998  cvmlift2lem11  25000  cvmlift2lem12  25001  cvmlift3lem6  25011  dfon2lem3  25412  dfon2lem7  25416  trpredpred  25506  wfrlem12  25549  wfrlem16  25553  frrlem11  25594  nobndlem2  25648  nobndlem8  25654  nofulllem3  25659  nofulllem5  25661  opnmbllem0  26242  mbfresfi  26253  ntruni  26330  clsint2  26332  comppfsc  26387  neibastop1  26388  topmeet  26393  topjoin  26394  fnemeet1  26395  fnejoin1  26397  heiborlem1  26520  isnacs3  26764  aomclem4  27132  kelac2  27140  stoweidlem28  27753  stoweidlem50  27775  stoweidlem52  27777  stoweidlem53  27778  stoweidlem54  27779  bnj1450  29419  bnj1501  29436  lssats  29810  dicval  31974  mapdunirnN  32448
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 2417
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 2423  df-cleq 2429  df-clel 2432  df-nfc 2561  df-v 2958  df-in 3327  df-ss 3334  df-uni 4016
  Copyright terms: Public domain W3C validator