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

Theorem elssuni 3753
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 3118 . 2  |-  A  C_  A
2 ssuni 3749 . 2  |-  ( ( A  C_  A  /\  A  e.  B )  ->  A  C_  U. B )
31, 2mpan 654 1  |-  ( A  e.  B  ->  A  C_ 
U. B )
Colors of variables: wff set class
Syntax hints:    -> wi 6    e. wcel 1621    C_ wss 3078   U.cuni 3727
This theorem is referenced by:  unissel  3754  ssunieq  3758  pwuni  4100  pwel  4119  uniopel  4163  iunpw  4461  dmrnssfld  4845  unixp0  5112  fvssunirn  5404  sorpssuni  6138  pwuninelALT  6185  onfununi  6244  tfrlem9  6287  tfrlem9a  6288  tfrlem13  6292  sbthlem1  6856  sbthlem2  6857  2pwuninel  6901  ordunifi  6992  unifpw  7042  fissuni  7044  dffi3  7068  cantnfp1lem3  7266  oemapvali  7270  cantnflem1  7275  cnfcom3lem  7290  rankuni2b  7409  carduni  7498  r0weon  7524  dfac8clem  7543  cardinfima  7608  alephfp  7619  iunfictbso  7625  dfac5lem4  7637  dfac2a  7640  dfacacn  7651  dfac12lem2  7654  kmlem2  7661  fin23lem16  7845  fin23lem21  7849  isf32lem5  7867  fin1a2lem11  7920  fin1a2lem13  7922  itunitc  7931  axdc2lem  7958  axdc3lem2  7961  ttukeylem5  8024  ttukeylem6  8025  fpwwe2lem11  8142  fpwwe2lem12  8143  fpwwe2lem13  8144  fpwwe2  8145  wunex2  8240  inatsk  8280  tskuni  8285  suplem1pr  8556  suplem2pr  8557  unirnioo  10621  mrcuni  13395  isacs3lem  14113  mrelatlub  14124  dprd2dlem1  15111  lbsextlem2  15744  eltopss  16485  toponss  16499  isbasis3g  16519  baspartn  16524  bastg  16536  tgcl  16539  fctop  16573  cctop  16575  ppttop  16576  epttop  16578  difopn  16603  ssntr  16627  isopn3  16635  isopn3i  16651  toponmre  16662  neiuni  16691  resttopon  16724  restopn2  16740  perfopn  16747  pnfnei  16782  mnfnei  16783  ssidcn  16817  lmcnp  16864  pnrmopn  16903  ist1-2  16907  nrmsep  16917  isnrm2  16918  isnrm3  16919  regsep2  16936  cncmp  16951  hauscmplem  16965  hauscmp  16966  conndisj  16974  cnconn  16980  concompss  16991  islly2  17042  nllyrest  17044  nllyidm  17047  hausllycmp  17052  cldllycmp  17053  lly1stc  17054  kgentopon  17065  kgenss  17070  llycmpkgen2  17077  1stckgen  17081  txuni2  17092  ptpjpre1  17098  ptuni2  17103  ptbasfi  17108  xkouni  17126  txcnpi  17134  ptpjopn  17138  txindis  17160  txnlly  17163  txtube  17166  hausdiag  17171  xkopt  17181  xkococnlem  17185  txcon  17215  qtopuni  17225  qtopkgen  17233  tgqtop  17235  regr1lem  17262  kqreglem1  17264  kqreglem2  17265  kqnrmlem1  17266  kqnrmlem2  17267  hmeoimaf1o  17293  reghmph  17316  nrmhmph  17317  filcon  17410  trfil1  17413  ufildr  17458  flimfil  17496  flimfnfcls  17555  alexsublem  17570  alexsubALTlem3  17575  tgioo  18134  xrtgioo  18144  xrsmopn  18150  opnreen  18168  cnheibor  18285  cnllycmp  18286  lebnumlem1  18291  lebnumlem3  18293  bcthlem5  18582  bcth2  18584  bcth3  18585  voliunlem1  18739  voliunlem3  18741  volsup  18745  opnmbllem  18788  mbfimaopnlem  18842  lhop  19195  ubthlem1  21279  shatomistici  22771  hatomistici  22772  pconcon  22933  cvmsf1o  22974  cvmscld  22975  cvmsss2  22976  cvmopnlem  22980  cvmfolem  22981  cvmliftmolem1  22983  cvmliftlem6  22992  cvmliftlem8  22994  cvmlift2lem9  23013  cvmlift2lem11  23015  cvmlift2lem12  23016  cvmlift3lem6  23026  dfon2lem3  23309  dfon2lem7  23313  trpredpred  23399  wfrlem12  23435  wfrlem16  23439  frrlem11  23461  axfelem2  23515  axfelem13  23526  axfelem18  23531  axfelem22  23535  unint2t  24684  intfmu2  24685  osneisi  24697  ntruni  25411  clsint2  25413  comppfsc  25473  neibastop1  25474  topmeet  25479  topjoin  25480  fnemeet1  25481  fnejoin1  25483  heiborlem1  25701  isnacs3  25951  aomclem4  26320  kelac2  26329  bnj1450  27769  bnj1501  27786  lssats  27891  dicval  30055  mapdunirnN  30529
This theorem was proved from axioms:  ax-1 7  ax-2 8  ax-3 9  ax-mp 10  ax-5 1533  ax-6 1534  ax-7 1535  ax-gen 1536  ax-8 1623  ax-11 1624  ax-17 1628  ax-12o 1664  ax-10 1678  ax-9 1684  ax-4 1692  ax-16 1926  ax-ext 2234
This theorem depends on definitions:  df-bi 179  df-or 361  df-an 362  df-tru 1315  df-ex 1538  df-nf 1540  df-sb 1883  df-clab 2240  df-cleq 2246  df-clel 2249  df-nfc 2374  df-v 2729  df-in 3085  df-ss 3089  df-uni 3728
  Copyright terms: Public domain W3C validator