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

Theorem elssuni 3856
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 3198 . 2  |-  A  C_  A
2 ssuni 3850 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 653 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1685    C_ wss 3153   U.cuni 3828
This theorem is referenced by:  unissel  3857  ssunieq  3861  pwuni  4205  pwel  4224  uniopel  4269  iunpw  4569  dmrnssfld  4937  unixp0  5204  fvssunirn  5512  sorpssuni  6247  pwuninelALT  6294  onfununi  6353  tfrlem9  6396  tfrlem9a  6397  tfrlem13  6401  sbthlem1  6966  sbthlem2  6967  2pwuninel  7011  ordunifi  7102  unifpw  7153  fissuni  7155  dffi3  7179  cantnfp1lem3  7377  oemapvali  7381  cantnflem1  7386  cnfcom3lem  7401  rankuni2b  7520  carduni  7609  r0weon  7635  dfac8clem  7654  cardinfima  7719  alephfp  7730  iunfictbso  7736  dfac5lem4  7748  dfac2a  7751  dfacacn  7762  dfac12lem2  7765  kmlem2  7772  fin23lem16  7956  fin23lem21  7960  isf32lem5  7978  fin1a2lem11  8031  fin1a2lem13  8033  itunitc  8042  axdc2lem  8069  axdc3lem2  8072  ttukeylem5  8135  ttukeylem6  8136  fpwwe2lem11  8257  fpwwe2lem12  8258  fpwwe2lem13  8259  fpwwe2  8260  wunex2  8355  inatsk  8395  tskuni  8400  suplem1pr  8671  suplem2pr  8672  unirnioo  10737  mrcuni  13517  isacs3lem  14263  mrelatlub  14283  dprd2dlem1  15270  lbsextlem2  15906  eltopss  16647  toponss  16661  isbasis3g  16681  baspartn  16686  bastg  16698  tgcl  16701  fctop  16735  cctop  16737  ppttop  16738  epttop  16740  difopn  16765  ssntr  16789  isopn3  16797  isopn3i  16813  toponmre  16824  neiuni  16853  resttopon  16886  restopn2  16902  perfopn  16909  pnfnei  16944  mnfnei  16945  ssidcn  16979  lmcnp  17026  pnrmopn  17065  ist1-2  17069  nrmsep  17079  isnrm2  17080  isnrm3  17081  regsep2  17098  cncmp  17113  hauscmplem  17127  hauscmp  17128  conndisj  17136  cnconn  17142  concompss  17153  islly2  17204  nllyrest  17206  nllyidm  17209  hausllycmp  17214  cldllycmp  17215  lly1stc  17216  kgentopon  17227  kgenss  17232  llycmpkgen2  17239  1stckgen  17243  txuni2  17254  ptpjpre1  17260  ptuni2  17265  ptbasfi  17270  xkouni  17288  txcnpi  17296  ptpjopn  17300  txindis  17322  txnlly  17325  txtube  17328  hausdiag  17333  xkopt  17343  xkococnlem  17347  txcon  17377  qtopuni  17387  qtopkgen  17395  tgqtop  17397  regr1lem  17424  kqreglem1  17426  kqreglem2  17427  kqnrmlem1  17428  kqnrmlem2  17429  hmeoimaf1o  17455  reghmph  17478  nrmhmph  17479  filcon  17572  trfil1  17575  ufildr  17620  flimfil  17658  flimfnfcls  17717  alexsublem  17732  alexsubALTlem3  17737  tgioo  18296  xrtgioo  18306  xrsmopn  18312  opnreen  18330  cnheibor  18447  cnllycmp  18448  lebnumlem1  18453  lebnumlem3  18455  bcthlem5  18744  bcth2  18746  bcth3  18747  voliunlem1  18901  voliunlem3  18903  volsup  18907  opnmbllem  18950  mbfimaopnlem  19004  lhop  19357  ubthlem1  21441  shatomistici  22933  hatomistici  22934  pconcon  23166  cvmsf1o  23207  cvmscld  23208  cvmsss2  23209  cvmopnlem  23213  cvmfolem  23214  cvmliftmolem1  23216  cvmliftlem6  23225  cvmliftlem8  23227  cvmlift2lem9  23246  cvmlift2lem11  23248  cvmlift2lem12  23249  cvmlift3lem6  23259  dfon2lem3  23542  dfon2lem7  23546  trpredpred  23632  wfrlem12  23668  wfrlem16  23672  frrlem11  23694  axfelem2  23748  axfelem13  23759  axfelem18  23764  axfelem22  23768  unint2t  24917  intfmu2  24918  osneisi  24930  ntruni  25644  clsint2  25646  comppfsc  25706  neibastop1  25707  topmeet  25712  topjoin  25713  fnemeet1  25714  fnejoin1  25716  heiborlem1  25934  isnacs3  26184  aomclem4  26553  kelac2  26562  stoweidlem28  27176  stoweidlem50  27198  stoweidlem52  27200  stoweidlem53  27201  stoweidlem54  27202  bnj1450  28347  bnj1501  28364  lssats  28469  dicval  30633  mapdunirnN  31107
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-gen 1534  ax-5 1545  ax-17 1604  ax-9 1637  ax-8 1645  ax-6 1704  ax-7 1709  ax-11 1716  ax-12 1867  ax-ext 2265
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1312  df-ex 1530  df-nf 1533  df-sb 1632  df-clab 2271  df-cleq 2277  df-clel 2280  df-nfc 2409  df-v 2791  df-in 3160  df-ss 3167  df-uni 3829
  Copyright terms: Public domain W3C validator