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

Theorem elssuni 4672
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 3831 . 2 𝐴𝐴
2 ssuni 4665 . 2 ((𝐴𝐴𝐴𝐵) → 𝐴 𝐵)
31, 2mpan 673 1 (𝐴𝐵𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  wss 3780   cuni 4641
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1877  ax-4 1894  ax-5 2001  ax-6 2069  ax-7 2105  ax-9 2166  ax-10 2186  ax-11 2202  ax-12 2215  ax-13 2422  ax-ext 2795
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-tru 1641  df-ex 1860  df-nf 1864  df-sb 2062  df-clab 2804  df-cleq 2810  df-clel 2813  df-nfc 2948  df-v 3404  df-in 3787  df-ss 3794  df-uni 4642
This theorem is referenced by:  unissel  4673  ssunieq  4677  pwuni  4679  pwel  5123  uniopel  5184  dmrnssfld  5599  unixp0  5897  fvssunirn  6447  sorpssuni  7186  iunpw  7218  pwuninel2  7645  wfrlem12  7672  wfrlem16  7676  wfrlem17  7677  onfununi  7684  tfrlem9  7727  tfrlem9a  7728  tfrlem13  7732  sbthlem1  8319  sbthlem2  8320  2pwuninel  8364  ordunifi  8459  unifpw  8518  fissuni  8520  dffi3  8586  cantnfp1lem3  8834  oemapvali  8838  cantnflem1  8843  cnfcom3lem  8857  rankuni2b  8973  carduni  9100  r0weon  9128  dfac8clem  9148  cardinfima  9213  alephfp  9224  iunfictbso  9230  dfac5lem4  9242  dfac2a  9245  dfacacn  9258  dfac12lem2  9261  kmlem2  9268  fin23lem16  9452  fin23lem21  9456  isf32lem5  9474  fin1a2lem11  9527  fin1a2lem13  9529  itunitc  9538  axdc2lem  9565  axdc3lem2  9568  ttukeylem5  9630  ttukeylem6  9631  fpwwe2lem11  9757  fpwwe2lem12  9758  fpwwe2lem13  9759  fpwwe2  9760  wunex2  9855  inatsk  9895  tskuni  9900  suplem1pr  10169  suplem2pr  10170  unirnioo  12512  mrcuni  16506  isacs3lem  17391  mrelatlub  17411  dprd2dlem1  18662  lbsextlem2  19388  eltopss  20946  toponss  20966  isbasis3g  20988  baspartn  20993  bastg  21005  tgcl  21008  fctop  21043  cctop  21045  ppttop  21046  epttop  21048  difopn  21073  ssntr  21097  isopn3  21105  isopn3i  21121  toponmre  21132  neiuni  21161  neiptoptop  21170  resttopon  21200  restopn2  21216  perfopn  21224  pnfnei  21259  mnfnei  21260  ssidcn  21294  lmcnp  21343  pnrmopn  21382  ist1-2  21386  nrmsep  21396  isnrm2  21397  isnrm3  21398  regsep2  21415  cncmp  21430  hauscmplem  21444  hauscmp  21445  conndisj  21454  cnconn  21460  conncompss  21471  islly2  21522  nllyrest  21524  nllyidm  21527  hausllycmp  21532  cldllycmp  21533  lly1stc  21534  comppfsc  21570  kgentopon  21576  kgenss  21581  llycmpkgen2  21588  1stckgen  21592  txuni2  21603  ptpjpre1  21609  ptuni2  21614  ptbasfi  21619  xkouni  21637  txcnpi  21646  ptpjopn  21650  txindis  21672  txnlly  21675  txtube  21678  hausdiag  21683  xkopt  21693  xkococnlem  21697  txconn  21727  qtopuni  21740  qtopkgen  21748  tgqtop  21750  regr1lem  21777  kqreglem1  21779  kqreglem2  21780  kqnrmlem1  21781  kqnrmlem2  21782  hmeoimaf1o  21808  reghmph  21831  nrmhmph  21832  filconn  21921  trfil1  21924  ufildr  21969  flimfil  22007  flimfnfcls  22066  alexsublem  22082  alexsubALTlem3  22087  ustbas2  22263  tgioo  22833  xrtgioo  22843  xrsmopn  22849  opnreen  22868  cnheibor  22988  cnllycmp  22989  lebnumlem1  22994  lebnumlem3  22996  bcthlem5  23359  bcth3  23362  voliunlem1  23554  voliunlem3  23556  volsup  23560  opnmbllem  23605  mbfimaopnlem  23659  lhop  24016  tglnpt  25681  tglineintmo  25774  ubthlem1  28077  shatomistici  29571  hatomistici  29572  unifi3  29840  tpr2rico  30306  hasheuni  30495  difelsiga  30544  prob01  30823  probdsb  30832  totprobd  30836  probmeasb  30840  cndprobtot  30846  orvcelval  30878  bnj1450  31463  bnj1501  31480  pconnconn  31558  cvmsf1o  31599  cvmscld  31600  cvmsss2  31601  cvmopnlem  31605  cvmfolem  31606  cvmliftmolem1  31608  cvmliftlem6  31617  cvmliftlem8  31619  cvmlift2lem9  31638  cvmlift2lem11  31640  cvmlift2lem12  31641  cvmlift3lem6  31651  dfon2lem3  32032  dfon2lem7  32036  trpredpred  32070  frrlem11  32135  nosupno  32192  nosupbday  32194  noetalem3  32208  ntruni  32665  clsint2  32667  neibastop1  32697  topmeet  32702  topjoin  32703  fnemeet1  32704  fnejoin1  32706  opnmbllem0  33777  mbfresfi  33787  heiborlem1  33940  lssats  34811  dicval  36975  mapdunirnN  37449  isnacs3  37793  aomclem4  38146  kelac2  38154  ssuniint  39761  stoweidlem28  40742  stoweidlem50  40764  stoweidlem52  40766  stoweidlem53  40767  stoweidlem54  40768  prsal  41035  salincl  41040  saliincl  41042  saldifcl2  41043  salexct  41049  psmeasurelem  41184  caragenuni  41225  carageniuncl  41237  caratheodorylem1  41240  caratheodorylem2  41241  voncmpl  41335  setrec1lem2  43021  setrec2fun  43025
  Copyright terms: Public domain W3C validator