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

Theorem elssuni 4903
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 3971 . 2 𝐴𝐴
2 ssuni 4898 . 2 ((𝐴𝐴𝐴𝐵) → 𝐴 𝐵)
31, 2mpan 689 1 (𝐴𝐵𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2107  wss 3915   cuni 4870
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2708
This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2715  df-cleq 2729  df-clel 2815  df-v 3450  df-in 3922  df-ss 3932  df-uni 4871
This theorem is referenced by:  unissel  4904  ssunieq  4909  pwuni  4911  pwel  5341  uniopel  5478  dmrnssfld  5930  unixp0  6240  elfvunirn  6879  fvssunirnOLD  6881  sorpssuni  7674  iunpw  7710  pwuninel2  8210  frrlem8  8229  frrlem10  8231  frrlem14  8235  fprresex  8246  wfrlem12OLD  8271  wfrlem16OLD  8275  wfrlem17OLD  8276  onfununi  8292  tfrlem9  8336  tfrlem9a  8337  tfrlem13  8341  sbthlem1  9034  sbthlem2  9035  2pwuninel  9083  ordunifi  9244  unifpw  9306  fissuni  9308  dffi3  9374  cantnfp1lem3  9623  oemapvali  9627  cantnflem1  9632  cnfcom3lem  9646  rankuni2b  9796  carduni  9924  r0weon  9955  dfac8clem  9975  cardinfima  10040  alephfp  10051  iunfictbso  10057  dfac5lem4  10069  dfac2a  10072  dfacacn  10084  dfac12lem2  10087  kmlem2  10094  fin23lem16  10278  fin23lem21  10282  isf32lem5  10300  fin1a2lem11  10353  fin1a2lem13  10355  itunitc  10364  axdc2lem  10391  axdc3lem2  10394  ttukeylem5  10456  ttukeylem6  10457  fpwwe2lem10  10583  fpwwe2lem11  10584  fpwwe2lem12  10585  fpwwe2  10586  wunex2  10681  inatsk  10721  tskuni  10726  suplem1pr  10995  suplem2pr  10996  unirnioo  13373  mrcuni  17508  isacs3lem  18438  mrelatlub  18458  dprd2dlem1  19827  lbsextlem2  20636  eltopss  22272  toponss  22292  isbasis3g  22315  baspartn  22320  bastg  22332  tgcl  22335  fctop  22370  cctop  22372  ppttop  22373  epttop  22375  difopn  22401  ssntr  22425  isopn3  22433  isopn3i  22449  toponmre  22460  neiuni  22489  neiptoptop  22498  resttopon  22528  restopn2  22544  perfopn  22552  pnfnei  22587  mnfnei  22588  ssidcn  22622  lmcnp  22671  pnrmopn  22710  ist1-2  22714  nrmsep  22724  isnrm2  22725  isnrm3  22726  regsep2  22743  cncmp  22759  hauscmplem  22773  hauscmp  22774  conndisj  22783  cnconn  22789  conncompss  22800  islly2  22851  nllyrest  22853  nllyidm  22856  hausllycmp  22861  cldllycmp  22862  lly1stc  22863  comppfsc  22899  kgentopon  22905  kgenss  22910  llycmpkgen2  22917  1stckgen  22921  txuni2  22932  ptpjpre1  22938  ptuni2  22943  ptbasfi  22948  xkouni  22966  txcnpi  22975  ptpjopn  22979  txindis  23001  txnlly  23004  txtube  23007  hausdiag  23012  xkopt  23022  xkococnlem  23026  txconn  23056  qtopuni  23069  qtopkgen  23077  tgqtop  23079  regr1lem  23106  kqreglem1  23108  kqreglem2  23109  kqnrmlem1  23110  kqnrmlem2  23111  hmeoimaf1o  23137  reghmph  23160  nrmhmph  23161  filconn  23250  trfil1  23253  ufildr  23298  flimfil  23336  flimfnfcls  23395  alexsublem  23411  alexsubALTlem3  23416  ustbas2  23593  tgioo  24175  xrtgioo  24185  xrsmopn  24191  opnreen  24210  cnheibor  24334  cnllycmp  24335  lebnumlem1  24340  lebnumlem3  24342  bcthlem5  24708  bcth3  24711  voliunlem1  24930  voliunlem3  24932  volsup  24936  opnmbllem  24981  mbfimaopnlem  25035  lhop  25396  nosupno  27067  noinfno  27082  noetasuplem4  27100  noetainflem4  27104  tglnpt  27533  tglineintmo  27626  ubthlem1  29854  shatomistici  31345  hatomistici  31346  unifi3  31671  elrspunidl  32243  zarclsiin  32492  tpr2rico  32533  hasheuni  32724  difelsiga  32772  prob01  33053  probdsb  33062  totprobd  33066  probmeasb  33070  cndprobtot  33076  orvcelval  33108  bnj1450  33702  bnj1501  33719  pconnconn  33865  cvmsf1o  33906  cvmscld  33907  cvmsss2  33908  cvmopnlem  33912  cvmfolem  33913  cvmliftmolem1  33915  cvmliftlem6  33924  cvmliftlem8  33926  cvmlift2lem9  33945  cvmlift2lem11  33947  cvmlift2lem12  33948  cvmlift3lem6  33958  dfon2lem3  34399  dfon2lem7  34403  ntruni  34828  clsint2  34830  neibastop1  34860  topmeet  34865  topjoin  34866  fnemeet1  34867  fnejoin1  34869  opnmbllem0  36143  mbfresfi  36153  heiborlem1  36299  lssats  37503  dicval  39668  mapdunirnN  40142  isnacs3  41062  aomclem4  41413  kelac2  41421  onsupuni  41592  onsupmaxb  41602  mnuunid  42631  mnutrcld  42633  grumnudlem  42639  ssuniint  43362  stoweidlem28  44343  stoweidlem50  44365  stoweidlem52  44367  stoweidlem53  44368  stoweidlem54  44369  prsal  44633  salincl  44639  saliinclf  44641  saldifcl2  44643  salexct  44649  psmeasurelem  44785  caragenuni  44826  carageniuncl  44838  caratheodorylem1  44841  caratheodorylem2  44842  voncmpl  44936  opncldeqv  47008  opndisj  47009  unilbeu  47084  setrec1lem2  47207  setrec2fun  47211
  Copyright terms: Public domain W3C validator