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

Theorem elssuni 4397
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 3586 . 2 𝐴𝐴
2 ssuni 4389 . 2 ((𝐴𝐴𝐴𝐵) → 𝐴 𝐵)
31, 2mpan 701 1 (𝐴𝐵𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  wss 3539   cuni 4366
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1712  ax-4 1727  ax-5 1826  ax-6 1874  ax-7 1921  ax-10 2005  ax-11 2020  ax-12 2032  ax-13 2232  ax-ext 2589
This theorem depends on definitions:  df-bi 195  df-or 383  df-an 384  df-tru 1477  df-ex 1695  df-nf 1700  df-sb 1867  df-clab 2596  df-cleq 2602  df-clel 2605  df-nfc 2739  df-v 3174  df-in 3546  df-ss 3553  df-uni 4367
This theorem is referenced by:  unissel  4398  ssunieq  4402  pwuni  4820  pwel  4841  uniopel  4894  dmrnssfld  5292  unixp0  5572  fvssunirn  6112  sorpssuni  6821  iunpw  6847  pwuninel2  7264  wfrlem12  7290  wfrlem16  7294  wfrlem17  7295  onfununi  7302  tfrlem9  7345  tfrlem9a  7346  tfrlem13  7350  sbthlem1  7932  sbthlem2  7933  2pwuninel  7977  ordunifi  8072  unifpw  8129  fissuni  8131  dffi3  8197  cantnfp1lem3  8437  oemapvali  8441  cantnflem1  8446  cnfcom3lem  8460  rankuni2b  8576  carduni  8667  r0weon  8695  dfac8clem  8715  cardinfima  8780  alephfp  8791  iunfictbso  8797  dfac5lem4  8809  dfac2a  8812  dfacacn  8823  dfac12lem2  8826  kmlem2  8833  fin23lem16  9017  fin23lem21  9021  isf32lem5  9039  fin1a2lem11  9092  fin1a2lem13  9094  itunitc  9103  axdc2lem  9130  axdc3lem2  9133  ttukeylem5  9195  ttukeylem6  9196  fpwwe2lem11  9318  fpwwe2lem12  9319  fpwwe2lem13  9320  fpwwe2  9321  wunex2  9416  inatsk  9456  tskuni  9461  suplem1pr  9730  suplem2pr  9731  unirnioo  12100  mrcuni  16050  isacs3lem  16935  mrelatlub  16955  dprd2dlem1  18209  lbsextlem2  18926  eltopss  20479  toponss  20486  isbasis3g  20506  baspartn  20511  bastg  20523  tgcl  20526  fctop  20560  cctop  20562  ppttop  20563  epttop  20565  difopn  20590  ssntr  20614  isopn3  20622  isopn3i  20638  toponmre  20649  neiuni  20678  neiptoptop  20687  resttopon  20717  restopn2  20733  perfopn  20741  pnfnei  20776  mnfnei  20777  ssidcn  20811  lmcnp  20860  pnrmopn  20899  ist1-2  20903  nrmsep  20913  isnrm2  20914  isnrm3  20915  regsep2  20932  cncmp  20947  hauscmplem  20961  hauscmp  20962  conndisj  20971  cnconn  20977  concompss  20988  islly2  21039  nllyrest  21041  nllyidm  21044  hausllycmp  21049  cldllycmp  21050  lly1stc  21051  comppfsc  21087  kgentopon  21093  kgenss  21098  llycmpkgen2  21105  1stckgen  21109  txuni2  21120  ptpjpre1  21126  ptuni2  21131  ptbasfi  21136  xkouni  21154  txcnpi  21163  ptpjopn  21167  txindis  21189  txnlly  21192  txtube  21195  hausdiag  21200  xkopt  21210  xkococnlem  21214  txcon  21244  qtopuni  21257  qtopkgen  21265  tgqtop  21267  regr1lem  21294  kqreglem1  21296  kqreglem2  21297  kqnrmlem1  21298  kqnrmlem2  21299  hmeoimaf1o  21325  reghmph  21348  nrmhmph  21349  filcon  21439  trfil1  21442  ufildr  21487  flimfil  21525  flimfnfcls  21584  alexsublem  21600  alexsubALTlem3  21605  ustbas2  21781  tgioo  22339  xrtgioo  22349  xrsmopn  22355  opnreen  22374  cnheibor  22493  cnllycmp  22494  lebnumlem1  22499  lebnumlem3  22501  bcthlem5  22850  bcth3  22853  voliunlem1  23042  voliunlem3  23044  volsup  23048  opnmbllem  23092  mbfimaopnlem  23145  lhop  23500  tglnpt  25162  tglineintmo  25255  ubthlem1  26916  shatomistici  28410  hatomistici  28411  unifi3  28679  tpr2rico  29092  hasheuni  29280  difelsiga  29329  prob01  29608  probdsb  29617  totprobd  29621  probmeasb  29625  cndprobtot  29631  orvcelval  29663  bnj1450  30178  bnj1501  30195  pconcon  30273  cvmsf1o  30314  cvmscld  30315  cvmsss2  30316  cvmopnlem  30320  cvmfolem  30321  cvmliftmolem1  30323  cvmliftlem6  30332  cvmliftlem8  30334  cvmlift2lem9  30353  cvmlift2lem11  30355  cvmlift2lem12  30356  cvmlift3lem6  30366  dfon2lem3  30740  dfon2lem7  30744  trpredpred  30778  frrlem11  30842  nobndlem2  30898  nobndlem8  30904  nofulllem3  30909  nofulllem5  30911  ntruni  31298  clsint2  31300  neibastop1  31330  topmeet  31335  topjoin  31336  fnemeet1  31337  fnejoin1  31339  opnmbllem0  32418  mbfresfi  32429  heiborlem1  32583  lssats  33120  dicval  35286  mapdunirnN  35760  isnacs3  36094  aomclem4  36448  kelac2  36456  ssuniint  38079  stoweidlem28  38725  stoweidlem50  38747  stoweidlem52  38749  stoweidlem53  38750  stoweidlem54  38751  prsal  39018  salincl  39023  saliincl  39025  saldifcl2  39026  salexct  39032  psmeasurelem  39167  caragenuni  39205  carageniuncl  39217  caratheodorylem1  39220  caratheodorylem2  39221  voncmpl  39315
  Copyright terms: Public domain W3C validator