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

Theorem elssuni 3855
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 3197 . 2  |-  A  C_  A
2 ssuni 3849 . 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 1684    C_ wss 3152   U.cuni 3827
This theorem is referenced by:  unissel  3856  ssunieq  3860  pwuni  4206  pwel  4225  uniopel  4270  iunpw  4570  dmrnssfld  4938  unixp0  5206  fvssunirn  5551  sorpssuni  6286  pwuninel2  6299  onfununi  6358  tfrlem9  6401  tfrlem9a  6402  tfrlem13  6406  sbthlem1  6971  sbthlem2  6972  2pwuninel  7016  ordunifi  7107  unifpw  7158  fissuni  7160  dffi3  7184  cantnfp1lem3  7382  oemapvali  7386  cantnflem1  7391  cnfcom3lem  7406  rankuni2b  7525  carduni  7614  r0weon  7640  dfac8clem  7659  cardinfima  7724  alephfp  7735  iunfictbso  7741  dfac5lem4  7753  dfac2a  7756  dfacacn  7767  dfac12lem2  7770  kmlem2  7777  fin23lem16  7961  fin23lem21  7965  isf32lem5  7983  fin1a2lem11  8036  fin1a2lem13  8038  itunitc  8047  axdc2lem  8074  axdc3lem2  8077  ttukeylem5  8140  ttukeylem6  8141  fpwwe2lem11  8262  fpwwe2lem12  8263  fpwwe2lem13  8264  fpwwe2  8265  wunex2  8360  inatsk  8400  tskuni  8405  suplem1pr  8676  suplem2pr  8677  unirnioo  10743  mrcuni  13523  isacs3lem  14269  mrelatlub  14289  dprd2dlem1  15276  lbsextlem2  15912  eltopss  16653  toponss  16667  isbasis3g  16687  baspartn  16692  bastg  16704  tgcl  16707  fctop  16741  cctop  16743  ppttop  16744  epttop  16746  difopn  16771  ssntr  16795  isopn3  16803  isopn3i  16819  toponmre  16830  neiuni  16859  resttopon  16892  restopn2  16908  perfopn  16915  pnfnei  16950  mnfnei  16951  ssidcn  16985  lmcnp  17032  pnrmopn  17071  ist1-2  17075  nrmsep  17085  isnrm2  17086  isnrm3  17087  regsep2  17104  cncmp  17119  hauscmplem  17133  hauscmp  17134  conndisj  17142  cnconn  17148  concompss  17159  islly2  17210  nllyrest  17212  nllyidm  17215  hausllycmp  17220  cldllycmp  17221  lly1stc  17222  kgentopon  17233  kgenss  17238  llycmpkgen2  17245  1stckgen  17249  txuni2  17260  ptpjpre1  17266  ptuni2  17271  ptbasfi  17276  xkouni  17294  txcnpi  17302  ptpjopn  17306  txindis  17328  txnlly  17331  txtube  17334  hausdiag  17339  xkopt  17349  xkococnlem  17353  txcon  17383  qtopuni  17393  qtopkgen  17401  tgqtop  17403  regr1lem  17430  kqreglem1  17432  kqreglem2  17433  kqnrmlem1  17434  kqnrmlem2  17435  hmeoimaf1o  17461  reghmph  17484  nrmhmph  17485  filcon  17578  trfil1  17581  ufildr  17626  flimfil  17664  flimfnfcls  17723  alexsublem  17738  alexsubALTlem3  17743  tgioo  18302  xrtgioo  18312  xrsmopn  18318  opnreen  18336  cnheibor  18453  cnllycmp  18454  lebnumlem1  18459  lebnumlem3  18461  bcthlem5  18750  bcth2  18752  bcth3  18753  voliunlem1  18907  voliunlem3  18909  volsup  18913  opnmbllem  18956  mbfimaopnlem  19010  lhop  19363  ubthlem1  21449  shatomistici  22941  hatomistici  22942  pconcon  23173  cvmsf1o  23214  cvmscld  23215  cvmsss2  23216  cvmopnlem  23220  cvmfolem  23221  cvmliftmolem1  23223  cvmliftlem6  23232  cvmliftlem8  23234  cvmlift2lem9  23253  cvmlift2lem11  23255  cvmlift2lem12  23256  cvmlift3lem6  23266  dfon2lem3  23552  dfon2lem7  23556  trpredpred  23642  wfrlem12  23678  wfrlem16  23682  frrlem11  23704  nobndlem2  23758  nobndlem8  23764  nofulllem3  23769  nofulllem5  23771  unint2t  24930  intfmu2  24931  osneisi  24943  ntruni  25657  clsint2  25659  comppfsc  25719  neibastop1  25720  topmeet  25725  topjoin  25726  fnemeet1  25727  fnejoin1  25729  heiborlem1  25947  isnacs3  26197  aomclem4  26566  kelac2  26575  stoweidlem28  27189  stoweidlem50  27211  stoweidlem52  27213  stoweidlem53  27214  stoweidlem54  27215  bnj1450  28453  bnj1501  28470  lssats  28575  dicval  30739  mapdunirnN  31213
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-v 2790  df-in 3159  df-ss 3166  df-uni 3828
  Copyright terms: Public domain W3C validator