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

Theorem elssuni 4458
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 3616 . 2 𝐴𝐴
2 ssuni 4450 . 2 ((𝐴𝐴𝐴𝐵) → 𝐴 𝐵)
31, 2mpan 705 1 (𝐴𝐵𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  wss 3567   cuni 4427
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1720  ax-4 1735  ax-5 1837  ax-6 1886  ax-7 1933  ax-9 1997  ax-10 2017  ax-11 2032  ax-12 2045  ax-13 2244  ax-ext 2600
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1484  df-ex 1703  df-nf 1708  df-sb 1879  df-clab 2607  df-cleq 2613  df-clel 2616  df-nfc 2751  df-v 3197  df-in 3574  df-ss 3581  df-uni 4428
This theorem is referenced by:  unissel  4459  ssunieq  4463  pwuni  4465  pwel  4911  uniopel  4968  dmrnssfld  5373  unixp0  5657  fvssunirn  6204  sorpssuni  6931  iunpw  6963  pwuninel2  7385  wfrlem12  7411  wfrlem16  7415  wfrlem17  7416  onfununi  7423  tfrlem9  7466  tfrlem9a  7467  tfrlem13  7471  sbthlem1  8055  sbthlem2  8056  2pwuninel  8100  ordunifi  8195  unifpw  8254  fissuni  8256  dffi3  8322  cantnfp1lem3  8562  oemapvali  8566  cantnflem1  8571  cnfcom3lem  8585  rankuni2b  8701  carduni  8792  r0weon  8820  dfac8clem  8840  cardinfima  8905  alephfp  8916  iunfictbso  8922  dfac5lem4  8934  dfac2a  8937  dfacacn  8948  dfac12lem2  8951  kmlem2  8958  fin23lem16  9142  fin23lem21  9146  isf32lem5  9164  fin1a2lem11  9217  fin1a2lem13  9219  itunitc  9228  axdc2lem  9255  axdc3lem2  9258  ttukeylem5  9320  ttukeylem6  9321  fpwwe2lem11  9447  fpwwe2lem12  9448  fpwwe2lem13  9449  fpwwe2  9450  wunex2  9545  inatsk  9585  tskuni  9590  suplem1pr  9859  suplem2pr  9860  unirnioo  12258  mrcuni  16262  isacs3lem  17147  mrelatlub  17167  dprd2dlem1  18421  lbsextlem2  19140  eltopss  20693  toponss  20712  isbasis3g  20734  baspartn  20739  bastg  20751  tgcl  20754  fctop  20789  cctop  20791  ppttop  20792  epttop  20794  difopn  20819  ssntr  20843  isopn3  20851  isopn3i  20867  toponmre  20878  neiuni  20907  neiptoptop  20916  resttopon  20946  restopn2  20962  perfopn  20970  pnfnei  21005  mnfnei  21006  ssidcn  21040  lmcnp  21089  pnrmopn  21128  ist1-2  21132  nrmsep  21142  isnrm2  21143  isnrm3  21144  regsep2  21161  cncmp  21176  hauscmplem  21190  hauscmp  21191  conndisj  21200  cnconn  21206  conncompss  21217  islly2  21268  nllyrest  21270  nllyidm  21273  hausllycmp  21278  cldllycmp  21279  lly1stc  21280  comppfsc  21316  kgentopon  21322  kgenss  21327  llycmpkgen2  21334  1stckgen  21338  txuni2  21349  ptpjpre1  21355  ptuni2  21360  ptbasfi  21365  xkouni  21383  txcnpi  21392  ptpjopn  21396  txindis  21418  txnlly  21421  txtube  21424  hausdiag  21429  xkopt  21439  xkococnlem  21443  txconn  21473  qtopuni  21486  qtopkgen  21494  tgqtop  21496  regr1lem  21523  kqreglem1  21525  kqreglem2  21526  kqnrmlem1  21527  kqnrmlem2  21528  hmeoimaf1o  21554  reghmph  21577  nrmhmph  21578  filconn  21668  trfil1  21671  ufildr  21716  flimfil  21754  flimfnfcls  21813  alexsublem  21829  alexsubALTlem3  21834  ustbas2  22010  tgioo  22580  xrtgioo  22590  xrsmopn  22596  opnreen  22615  cnheibor  22735  cnllycmp  22736  lebnumlem1  22741  lebnumlem3  22743  bcthlem5  23106  bcth3  23109  voliunlem1  23299  voliunlem3  23301  volsup  23305  opnmbllem  23350  mbfimaopnlem  23403  lhop  23760  tglnpt  25425  tglineintmo  25518  ubthlem1  27696  shatomistici  29190  hatomistici  29191  unifi3  29464  tpr2rico  29932  hasheuni  30121  difelsiga  30170  prob01  30449  probdsb  30458  totprobd  30462  probmeasb  30466  cndprobtot  30472  orvcelval  30504  bnj1450  31092  bnj1501  31109  pconnconn  31187  cvmsf1o  31228  cvmscld  31229  cvmsss2  31230  cvmopnlem  31234  cvmfolem  31235  cvmliftmolem1  31237  cvmliftlem6  31246  cvmliftlem8  31248  cvmlift2lem9  31267  cvmlift2lem11  31269  cvmlift2lem12  31270  cvmlift3lem6  31280  dfon2lem3  31664  dfon2lem7  31668  trpredpred  31702  frrlem11  31766  nosupno  31823  nosupbday  31825  noetalem3  31839  ntruni  32297  clsint2  32299  neibastop1  32329  topmeet  32334  topjoin  32335  fnemeet1  32336  fnejoin1  32338  opnmbllem0  33416  mbfresfi  33427  heiborlem1  33581  lssats  34118  dicval  36284  mapdunirnN  36758  isnacs3  37092  aomclem4  37446  kelac2  37454  ssuniint  39070  stoweidlem28  40008  stoweidlem50  40030  stoweidlem52  40032  stoweidlem53  40033  stoweidlem54  40034  prsal  40301  salincl  40306  saliincl  40308  saldifcl2  40309  salexct  40315  psmeasurelem  40450  caragenuni  40488  carageniuncl  40500  caratheodorylem1  40503  caratheodorylem2  40504  voncmpl  40598  setrec1lem2  42200  setrec2fun  42204
  Copyright terms: Public domain W3C validator