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  clduni  23289  tpr2rico  23296  hasheuni  23453  prob01  23616  probdsb  23625  totprobd  23629  probmeasb  23633  cndprobtot  23639  orvcelval  23669  pconcon  23762  cvmsf1o  23803  cvmscld  23804  cvmsss2  23805  cvmopnlem  23809  cvmfolem  23810  cvmliftmolem1  23812  cvmliftlem6  23821  cvmliftlem8  23823  cvmlift2lem9  23842  cvmlift2lem11  23844  cvmlift2lem12  23845  cvmlift3lem6  23855  dfon2lem3  24141  dfon2lem7  24145  trpredpred  24231  wfrlem12  24267  wfrlem16  24271  frrlem11  24293  nobndlem2  24347  nobndlem8  24353  nofulllem3  24358  nofulllem5  24360  unint2t  25518  intfmu2  25519  osneisi  25531  ntruni  26245  clsint2  26247  comppfsc  26307  neibastop1  26308  topmeet  26313  topjoin  26314  fnemeet1  26315  fnejoin1  26317  heiborlem1  26535  isnacs3  26785  aomclem4  27154  kelac2  27163  stoweidlem28  27777  stoweidlem50  27799  stoweidlem52  27801  stoweidlem53  27802  stoweidlem54  27803  bnj1450  29080  bnj1501  29097  lssats  29202  dicval  31366  mapdunirnN  31840
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