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

Theorem elssuni 4251
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 3489 . 2  |-  A  C_  A
2 ssuni 4244 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 674 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    e. wcel 1870    C_ wss 3442   U.cuni 4222
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407
This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449  df-ss 3456  df-uni 4223
This theorem is referenced by:  unissel  4252  ssunieq  4256  pwuni  4653  pwel  4674  uniopel  4725  dmrnssfld  5113  unixp0  5390  fvssunirn  5904  sorpssuni  6594  iunpw  6619  pwuninel2  7029  wfrlem12  7055  wfrlem16  7059  wfrlem17  7060  onfununi  7068  tfrlem9  7111  tfrlem9a  7112  tfrlem13  7116  sbthlem1  7688  sbthlem2  7689  2pwuninel  7733  ordunifi  7827  unifpw  7883  fissuni  7885  dffi3  7951  cantnfp1lem3  8184  oemapvali  8188  cantnflem1  8193  cnfcom3lem  8207  rankuni2b  8323  carduni  8414  r0weon  8442  dfac8clem  8461  cardinfima  8526  alephfp  8537  iunfictbso  8543  dfac5lem4  8555  dfac2a  8558  dfacacn  8569  dfac12lem2  8572  kmlem2  8579  fin23lem16  8763  fin23lem21  8767  isf32lem5  8785  fin1a2lem11  8838  fin1a2lem13  8840  itunitc  8849  axdc2lem  8876  axdc3lem2  8879  ttukeylem5  8941  ttukeylem6  8942  fpwwe2lem11  9064  fpwwe2lem12  9065  fpwwe2lem13  9066  fpwwe2  9067  wunex2  9162  inatsk  9202  tskuni  9207  suplem1pr  9476  suplem2pr  9477  unirnioo  11734  mrcuni  15478  isacs3lem  16363  mrelatlub  16383  dprd2dlem1  17609  lbsextlem2  18317  eltopss  19868  toponss  19875  isbasis3g  19895  baspartn  19900  bastg  19912  tgcl  19916  fctop  19950  cctop  19952  ppttop  19953  epttop  19955  difopn  19980  ssntr  20004  isopn3  20013  isopn3i  20029  toponmre  20040  neiuni  20069  neiptoptop  20078  resttopon  20108  restopn2  20124  perfopn  20132  pnfnei  20167  mnfnei  20168  ssidcn  20202  lmcnp  20251  pnrmopn  20290  ist1-2  20294  nrmsep  20304  isnrm2  20305  isnrm3  20306  regsep2  20323  cncmp  20338  hauscmplem  20352  hauscmp  20353  conndisj  20362  cnconn  20368  concompss  20379  islly2  20430  nllyrest  20432  nllyidm  20435  hausllycmp  20440  cldllycmp  20441  lly1stc  20442  comppfsc  20478  kgentopon  20484  kgenss  20489  llycmpkgen2  20496  1stckgen  20500  txuni2  20511  ptpjpre1  20517  ptuni2  20522  ptbasfi  20527  xkouni  20545  txcnpi  20554  ptpjopn  20558  txindis  20580  txnlly  20583  txtube  20586  hausdiag  20591  xkopt  20601  xkococnlem  20605  txcon  20635  qtopuni  20648  qtopkgen  20656  tgqtop  20658  regr1lem  20685  kqreglem1  20687  kqreglem2  20688  kqnrmlem1  20689  kqnrmlem2  20690  hmeoimaf1o  20716  reghmph  20739  nrmhmph  20740  filcon  20829  trfil1  20832  ufildr  20877  flimfil  20915  flimfnfcls  20974  alexsublem  20990  alexsubALTlem3  20995  ustbas2  21171  tgioo  21725  xrtgioo  21735  xrsmopn  21741  opnreen  21760  cnheibor  21879  cnllycmp  21880  lebnumlem1  21885  lebnumlem3  21887  bcthlem5  22189  bcth3  22192  voliunlem1  22380  voliunlem3  22382  volsup  22386  opnmbllem  22436  mbfimaopnlem  22488  lhop  22845  tglnpt  24454  tglineintmo  24546  ubthlem1  26357  shatomistici  27849  hatomistici  27850  unifi3  28132  tpr2rico  28557  hasheuni  28745  difelsiga  28794  prob01  29072  probdsb  29081  totprobd  29085  probmeasb  29089  cndprobtot  29095  orvcelval  29127  bnj1450  29647  bnj1501  29664  pconcon  29742  cvmsf1o  29783  cvmscld  29784  cvmsss2  29785  cvmopnlem  29789  cvmfolem  29790  cvmliftmolem1  29792  cvmliftlem6  29801  cvmliftlem8  29803  cvmlift2lem9  29822  cvmlift2lem11  29824  cvmlift2lem12  29825  cvmlift3lem6  29835  dfon2lem3  30218  dfon2lem7  30222  trpredpred  30256  frrlem11  30313  nobndlem2  30367  nobndlem8  30373  nofulllem3  30378  nofulllem5  30380  ntruni  30768  clsint2  30770  neibastop1  30800  topmeet  30805  topjoin  30806  fnemeet1  30807  fnejoin1  30809  opnmbllem0  31679  mbfresfi  31690  heiborlem1  31846  lssats  32286  dicval  34452  mapdunirnN  34926  isnacs3  35260  aomclem4  35620  kelac2  35628  stoweidlem28  37456  stoweidlem50  37479  stoweidlem52  37481  stoweidlem53  37482  stoweidlem54  37483  prsal  37725  salincl  37730  saliincl  37732  saldifcl2  37733  psmeasurelem  37816  caragenuni  37840  carageniuncl  37852  caratheodorylem1  37855  caratheodorylem2  37856
  Copyright terms: Public domain W3C validator