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

Theorem elssuni 4841
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 3965 . 2 𝐴𝐴
2 ssuni 4836 . 2 ((𝐴𝐴𝐴𝐵) → 𝐴 𝐵)
31, 2mpan 689 1 (𝐴𝐵𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2115  wss 3910   cuni 4811
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1971  ax-7 2016  ax-8 2117  ax-9 2125  ax-10 2146  ax-11 2162  ax-12 2178  ax-ext 2793
This theorem depends on definitions:  df-bi 210  df-an 400  df-or 845  df-tru 1541  df-ex 1782  df-nf 1786  df-sb 2071  df-clab 2800  df-cleq 2814  df-clel 2892  df-nfc 2960  df-v 3473  df-in 3917  df-ss 3927  df-uni 4812
This theorem is referenced by:  unissel  4842  ssunieq  4846  pwuni  4848  pwel  5255  uniopel  5379  dmrnssfld  5814  unixp0  6107  fvssunirn  6672  sorpssuni  7433  iunpw  7468  pwuninel2  7915  wfrlem12  7941  wfrlem16  7945  wfrlem17  7946  onfununi  7953  tfrlem9  7996  tfrlem9a  7997  tfrlem13  8001  sbthlem1  8603  sbthlem2  8604  2pwuninel  8648  ordunifi  8744  unifpw  8803  fissuni  8805  dffi3  8871  cantnfp1lem3  9119  oemapvali  9123  cantnflem1  9128  cnfcom3lem  9142  rankuni2b  9258  carduni  9386  r0weon  9415  dfac8clem  9435  cardinfima  9500  alephfp  9511  iunfictbso  9517  dfac5lem4  9529  dfac2a  9532  dfacacn  9544  dfac12lem2  9547  kmlem2  9554  fin23lem16  9734  fin23lem21  9738  isf32lem5  9756  fin1a2lem11  9809  fin1a2lem13  9811  itunitc  9820  axdc2lem  9847  axdc3lem2  9850  ttukeylem5  9912  ttukeylem6  9913  fpwwe2lem11  10039  fpwwe2lem12  10040  fpwwe2lem13  10041  fpwwe2  10042  wunex2  10137  inatsk  10177  tskuni  10182  suplem1pr  10451  suplem2pr  10452  unirnioo  12817  mrcuni  16870  isacs3lem  17754  mrelatlub  17774  dprd2dlem1  19141  lbsextlem2  19906  eltopss  21490  toponss  21510  isbasis3g  21532  baspartn  21537  bastg  21549  tgcl  21552  fctop  21587  cctop  21589  ppttop  21590  epttop  21592  difopn  21617  ssntr  21641  isopn3  21649  isopn3i  21665  toponmre  21676  neiuni  21705  neiptoptop  21714  resttopon  21744  restopn2  21760  perfopn  21768  pnfnei  21803  mnfnei  21804  ssidcn  21838  lmcnp  21887  pnrmopn  21926  ist1-2  21930  nrmsep  21940  isnrm2  21941  isnrm3  21942  regsep2  21959  cncmp  21975  hauscmplem  21989  hauscmp  21990  conndisj  21999  cnconn  22005  conncompss  22016  islly2  22067  nllyrest  22069  nllyidm  22072  hausllycmp  22077  cldllycmp  22078  lly1stc  22079  comppfsc  22115  kgentopon  22121  kgenss  22126  llycmpkgen2  22133  1stckgen  22137  txuni2  22148  ptpjpre1  22154  ptuni2  22159  ptbasfi  22164  xkouni  22182  txcnpi  22191  ptpjopn  22195  txindis  22217  txnlly  22220  txtube  22223  hausdiag  22228  xkopt  22238  xkococnlem  22242  txconn  22272  qtopuni  22285  qtopkgen  22293  tgqtop  22295  regr1lem  22322  kqreglem1  22324  kqreglem2  22325  kqnrmlem1  22326  kqnrmlem2  22327  hmeoimaf1o  22353  reghmph  22376  nrmhmph  22377  filconn  22466  trfil1  22469  ufildr  22514  flimfil  22552  flimfnfcls  22611  alexsublem  22627  alexsubALTlem3  22632  ustbas2  22809  tgioo  23379  xrtgioo  23389  xrsmopn  23395  opnreen  23414  cnheibor  23538  cnllycmp  23539  lebnumlem1  23544  lebnumlem3  23546  bcthlem5  23910  bcth3  23913  voliunlem1  24132  voliunlem3  24134  volsup  24138  opnmbllem  24183  mbfimaopnlem  24237  lhop  24597  tglnpt  26321  tglineintmo  26414  ubthlem1  28631  shatomistici  30122  hatomistici  30123  unifi3  30434  tpr2rico  31162  hasheuni  31351  difelsiga  31399  prob01  31678  probdsb  31687  totprobd  31691  probmeasb  31695  cndprobtot  31701  orvcelval  31733  bnj1450  32329  bnj1501  32346  pconnconn  32485  cvmsf1o  32526  cvmscld  32527  cvmsss2  32528  cvmopnlem  32532  cvmfolem  32533  cvmliftmolem1  32535  cvmliftlem6  32544  cvmliftlem8  32546  cvmlift2lem9  32565  cvmlift2lem11  32567  cvmlift2lem12  32568  cvmlift3lem6  32578  dfon2lem3  33037  dfon2lem7  33041  trpredpred  33074  frrlem8  33137  frrlem10  33139  frrlem14  33143  nosupno  33210  nosupbday  33212  noetalem3  33226  ntruni  33682  clsint2  33684  neibastop1  33714  topmeet  33719  topjoin  33720  fnemeet1  33721  fnejoin1  33723  opnmbllem0  34971  mbfresfi  34981  heiborlem1  35127  lssats  36186  dicval  38350  mapdunirnN  38824  isnacs3  39446  aomclem4  39796  kelac2  39804  mnuunid  40768  mnutrcld  40770  grumnudlem  40776  ssuniint  41497  stoweidlem28  42461  stoweidlem50  42483  stoweidlem52  42485  stoweidlem53  42486  stoweidlem54  42487  prsal  42751  salincl  42756  saliincl  42758  saldifcl2  42759  salexct  42765  psmeasurelem  42900  caragenuni  42941  carageniuncl  42953  caratheodorylem1  42956  caratheodorylem2  42957  voncmpl  43051  setrec1lem2  44978  setrec2fun  44982
  Copyright terms: Public domain W3C validator