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

Theorem elssuni 4607
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 3753 . 2 𝐴𝐴
2 ssuni 4599 . 2 ((𝐴𝐴𝐴𝐵) → 𝐴 𝐵)
31, 2mpan 708 1 (𝐴𝐵𝐴 𝐵)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2127  wss 3703   cuni 4576
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1859  ax-4 1874  ax-5 1976  ax-6 2042  ax-7 2078  ax-9 2136  ax-10 2156  ax-11 2171  ax-12 2184  ax-13 2379  ax-ext 2728
This theorem depends on definitions:  df-bi 197  df-or 384  df-an 385  df-tru 1623  df-ex 1842  df-nf 1847  df-sb 2035  df-clab 2735  df-cleq 2741  df-clel 2744  df-nfc 2879  df-v 3330  df-in 3710  df-ss 3717  df-uni 4577
This theorem is referenced by:  unissel  4608  ssunieq  4612  pwuni  4614  pwel  5057  uniopel  5114  dmrnssfld  5527  unixp0  5818  fvssunirn  6366  sorpssuni  7099  iunpw  7131  pwuninel2  7557  wfrlem12  7583  wfrlem16  7587  wfrlem17  7588  onfununi  7595  tfrlem9  7638  tfrlem9a  7639  tfrlem13  7643  sbthlem1  8223  sbthlem2  8224  2pwuninel  8268  ordunifi  8363  unifpw  8422  fissuni  8424  dffi3  8490  cantnfp1lem3  8738  oemapvali  8742  cantnflem1  8747  cnfcom3lem  8761  rankuni2b  8877  carduni  8968  r0weon  8996  dfac8clem  9016  cardinfima  9081  alephfp  9092  iunfictbso  9098  dfac5lem4  9110  dfac2a  9113  dfacacn  9126  dfac12lem2  9129  kmlem2  9136  fin23lem16  9320  fin23lem21  9324  isf32lem5  9342  fin1a2lem11  9395  fin1a2lem13  9397  itunitc  9406  axdc2lem  9433  axdc3lem2  9436  ttukeylem5  9498  ttukeylem6  9499  fpwwe2lem11  9625  fpwwe2lem12  9626  fpwwe2lem13  9627  fpwwe2  9628  wunex2  9723  inatsk  9763  tskuni  9768  suplem1pr  10037  suplem2pr  10038  unirnioo  12437  mrcuni  16454  isacs3lem  17338  mrelatlub  17358  dprd2dlem1  18611  lbsextlem2  19332  eltopss  20885  toponss  20904  isbasis3g  20926  baspartn  20931  bastg  20943  tgcl  20946  fctop  20981  cctop  20983  ppttop  20984  epttop  20986  difopn  21011  ssntr  21035  isopn3  21043  isopn3i  21059  toponmre  21070  neiuni  21099  neiptoptop  21108  resttopon  21138  restopn2  21154  perfopn  21162  pnfnei  21197  mnfnei  21198  ssidcn  21232  lmcnp  21281  pnrmopn  21320  ist1-2  21324  nrmsep  21334  isnrm2  21335  isnrm3  21336  regsep2  21353  cncmp  21368  hauscmplem  21382  hauscmp  21383  conndisj  21392  cnconn  21398  conncompss  21409  islly2  21460  nllyrest  21462  nllyidm  21465  hausllycmp  21470  cldllycmp  21471  lly1stc  21472  comppfsc  21508  kgentopon  21514  kgenss  21519  llycmpkgen2  21526  1stckgen  21530  txuni2  21541  ptpjpre1  21547  ptuni2  21552  ptbasfi  21557  xkouni  21575  txcnpi  21584  ptpjopn  21588  txindis  21610  txnlly  21613  txtube  21616  hausdiag  21621  xkopt  21631  xkococnlem  21635  txconn  21665  qtopuni  21678  qtopkgen  21686  tgqtop  21688  regr1lem  21715  kqreglem1  21717  kqreglem2  21718  kqnrmlem1  21719  kqnrmlem2  21720  hmeoimaf1o  21746  reghmph  21769  nrmhmph  21770  filconn  21859  trfil1  21862  ufildr  21907  flimfil  21945  flimfnfcls  22004  alexsublem  22020  alexsubALTlem3  22025  ustbas2  22201  tgioo  22771  xrtgioo  22781  xrsmopn  22787  opnreen  22806  cnheibor  22926  cnllycmp  22927  lebnumlem1  22932  lebnumlem3  22934  bcthlem5  23296  bcth3  23299  voliunlem1  23489  voliunlem3  23491  volsup  23495  opnmbllem  23540  mbfimaopnlem  23592  lhop  23949  tglnpt  25614  tglineintmo  25707  ubthlem1  28006  shatomistici  29500  hatomistici  29501  unifi3  29770  tpr2rico  30238  hasheuni  30427  difelsiga  30476  prob01  30755  probdsb  30764  totprobd  30768  probmeasb  30772  cndprobtot  30778  orvcelval  30810  bnj1450  31396  bnj1501  31413  pconnconn  31491  cvmsf1o  31532  cvmscld  31533  cvmsss2  31534  cvmopnlem  31538  cvmfolem  31539  cvmliftmolem1  31541  cvmliftlem6  31550  cvmliftlem8  31552  cvmlift2lem9  31571  cvmlift2lem11  31573  cvmlift2lem12  31574  cvmlift3lem6  31584  dfon2lem3  31966  dfon2lem7  31970  trpredpred  32004  frrlem11  32069  nosupno  32126  nosupbday  32128  noetalem3  32142  ntruni  32599  clsint2  32601  neibastop1  32631  topmeet  32636  topjoin  32637  fnemeet1  32638  fnejoin1  32640  opnmbllem0  33727  mbfresfi  33738  heiborlem1  33892  lssats  34771  dicval  36936  mapdunirnN  37410  isnacs3  37744  aomclem4  38098  kelac2  38106  ssuniint  39718  stoweidlem28  40717  stoweidlem50  40739  stoweidlem52  40741  stoweidlem53  40742  stoweidlem54  40743  prsal  41010  salincl  41015  saliincl  41017  saldifcl2  41018  salexct  41024  psmeasurelem  41159  caragenuni  41200  carageniuncl  41212  caratheodorylem1  41215  caratheodorylem2  41216  voncmpl  41310  setrec1lem2  42914  setrec2fun  42918
  Copyright terms: Public domain W3C validator