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

Theorem elssuni 4279
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

Proof of Theorem elssuni
StepHypRef Expression
1 ssid 3522 . 2
2 ssuni 4271 . 2
31, 2mpan 670 1
Colors of variables: wff setvar class
Syntax hints:  ->wi 4  e.wcel 1818  C_wss 3475  U.cuni 4249
This theorem is referenced by:  unissel  4280  ssunieq  4284  pwuni  4683  pwel  4704  uniopel  4756  dmrnssfld  5266  unixp0  5546  fvssunirn  5894  sorpssuni  6589  iunpw  6614  pwuninel2  7022  onfununi  7031  tfrlem9  7073  tfrlem9a  7074  tfrlem13  7078  sbthlem1  7647  sbthlem2  7648  2pwuninel  7692  ordunifi  7790  unifpw  7843  fissuni  7845  dffi3  7911  cantnfp1lem3  8120  oemapvali  8124  cantnflem1  8129  cantnfp1lem3OLD  8146  cantnflem1OLD  8152  cnfcom3lem  8168  cnfcom3lemOLD  8176  rankuni2b  8292  carduni  8383  r0weon  8411  dfac8clem  8434  cardinfima  8499  alephfp  8510  iunfictbso  8516  dfac5lem4  8528  dfac2a  8531  dfacacn  8542  dfac12lem2  8545  kmlem2  8552  fin23lem16  8736  fin23lem21  8740  isf32lem5  8758  fin1a2lem11  8811  fin1a2lem13  8813  itunitc  8822  axdc2lem  8849  axdc3lem2  8852  ttukeylem5  8914  ttukeylem6  8915  fpwwe2lem11  9039  fpwwe2lem12  9040  fpwwe2lem13  9041  fpwwe2  9042  wunex2  9137  inatsk  9177  tskuni  9182  suplem1pr  9451  suplem2pr  9452  unirnioo  11653  mrcuni  15018  isacs3lem  15796  mrelatlub  15816  dprd2dlem1  17090  lbsextlem2  17805  eltopss  19416  toponss  19430  isbasis3g  19450  baspartn  19455  bastg  19467  tgcl  19471  fctop  19505  cctop  19507  ppttop  19508  epttop  19510  difopn  19535  ssntr  19559  isopn3  19567  isopn3i  19583  toponmre  19594  neiuni  19623  neiptoptop  19632  resttopon  19662  restopn2  19678  perfopn  19686  pnfnei  19721  mnfnei  19722  ssidcn  19756  lmcnp  19805  pnrmopn  19844  ist1-2  19848  nrmsep  19858  isnrm2  19859  isnrm3  19860  regsep2  19877  cncmp  19892  hauscmplem  19906  hauscmp  19907  conndisj  19917  cnconn  19923  concompss  19934  islly2  19985  nllyrest  19987  nllyidm  19990  hausllycmp  19995  cldllycmp  19996  lly1stc  19997  comppfsc  20033  kgentopon  20039  kgenss  20044  llycmpkgen2  20051  1stckgen  20055  txuni2  20066  ptpjpre1  20072  ptuni2  20077  ptbasfi  20082  xkouni  20100  txcnpi  20109  ptpjopn  20113  txindis  20135  txnlly  20138  txtube  20141  hausdiag  20146  xkopt  20156  xkococnlem  20160  txcon  20190  qtopuni  20203  qtopkgen  20211  tgqtop  20213  regr1lem  20240  kqreglem1  20242  kqreglem2  20243  kqnrmlem1  20244  kqnrmlem2  20245  hmeoimaf1o  20271  reghmph  20294  nrmhmph  20295  filcon  20384  trfil1  20387  ufildr  20432  flimfil  20470  flimfnfcls  20529  alexsublem  20544  alexsubALTlem3  20549  ustbas2  20728  tgioo  21301  xrtgioo  21311  xrsmopn  21317  opnreen  21336  cnheibor  21455  cnllycmp  21456  lebnumlem1  21461  lebnumlem3  21463  bcthlem5  21767  bcth3  21770  voliunlem1  21960  voliunlem3  21962  volsup  21966  opnmbllem  22010  mbfimaopnlem  22062  lhop  22417  tglnpt  23936  tglineintmo  24022  ubthlem1  25786  shatomistici  27280  hatomistici  27281  unifi3  27528  tpr2rico  27894  hasheuni  28091  difelsiga  28133  prob01  28352  probdsb  28361  totprobd  28365  probmeasb  28369  cndprobtot  28375  orvcelval  28407  pconcon  28676  cvmsf1o  28717  cvmscld  28718  cvmsss2  28719  cvmopnlem  28723  cvmfolem  28724  cvmliftmolem1  28726  cvmliftlem6  28735  cvmliftlem8  28737  cvmlift2lem9  28756  cvmlift2lem11  28758  cvmlift2lem12  28759  cvmlift3lem6  28769  dfon2lem3  29217  dfon2lem7  29221  trpredpred  29311  wfrlem12  29354  wfrlem16  29358  frrlem11  29399  nobndlem2  29453  nobndlem8  29459  nofulllem3  29464  nofulllem5  29466  opnmbllem0  30050  mbfresfi  30061  ntruni  30145  clsint2  30147  neibastop1  30177  topmeet  30182  topjoin  30183  fnemeet1  30184  fnejoin1  30186  heiborlem1  30307  isnacs3  30642  aomclem4  31003  kelac2  31011  stoweidlem28  31810  stoweidlem50  31832  stoweidlem52  31834  stoweidlem53  31835  stoweidlem54  31836  bnj1450  34106  bnj1501  34123  lssats  34737  dicval  36903  mapdunirnN  37377
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482  df-ss 3489  df-uni 4250
  Copyright terms: Public domain W3C validator