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

Theorem elind 3782
Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)
Hypotheses
Ref Expression
elind.1 (𝜑𝑋𝐴)
elind.2 (𝜑𝑋𝐵)
Assertion
Ref Expression
elind (𝜑𝑋 ∈ (𝐴𝐵))

Proof of Theorem elind
StepHypRef Expression
1 elind.1 . 2 (𝜑𝑋𝐴)
2 elind.2 . 2 (𝜑𝑋𝐵)
3 elin 3780 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 697 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1987  cin 3559
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1719  ax-4 1734  ax-5 1836  ax-6 1885  ax-7 1932  ax-9 1996  ax-10 2016  ax-11 2031  ax-12 2044  ax-13 2245  ax-ext 2601
This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1483  df-ex 1702  df-nf 1707  df-sb 1878  df-clab 2608  df-cleq 2614  df-clel 2617  df-nfc 2750  df-v 3192  df-in 3567
This theorem is referenced by:  tfrlem5  7436  uniinqs  7787  unifpw  8229  f1opwfi  8230  fissuni  8231  fipreima  8232  elfir  8281  inelfi  8284  cantnfcl  8524  tskwe  8736  infpwfidom  8811  infpwfien  8845  ackbij2lem1  9001  ackbij1lem3  9004  ackbij1lem4  9005  ackbij1lem6  9007  ackbij1lem11  9012  fin23lem24  9104  isfin1-3  9168  fpwwe2lem12  9423  fpwwe  9428  canthnumlem  9430  fz1isolem  13199  isprm7  15363  setsstruct2  15836  strfv2d  15845  submre  16205  submrc  16228  isacs2  16254  coffth  16536  catcoppccl  16698  catcfuccl  16699  catcxpccl  16787  isdrs2  16879  fpwipodrs  17104  sylow2a  17974  lsmmod  18028  lsmdisj  18034  lsmdisj2  18035  subgdisj1  18044  frgpnabllem1  18216  dmdprdd  18338  dprdfeq0  18361  dprdres  18367  dprddisj2  18378  dprd2da  18381  dmdprdsplit2lem  18384  ablfacrp  18405  pgpfac1lem3a  18415  pgpfac1lem3  18416  pgpfaclem1  18420  aspval  19268  mplind  19442  zringlpirlem1  19772  zringlpirlem3  19774  pmatcoe1fsupp  20446  baspartn  20698  bastg  20710  clsval2  20794  isopn3  20810  restbas  20902  lmss  21042  cmpcovf  21134  discmp  21141  cmpsublem  21142  cmpsub  21143  isconn2  21157  connclo  21158  llynlly  21220  restnlly  21225  restlly  21226  islly2  21227  llyrest  21228  nllyrest  21229  llyidm  21231  nllyidm  21232  hausllycmp  21237  cldllycmp  21238  lly1stc  21239  dislly  21240  llycmpkgen2  21293  1stckgenlem  21296  txlly  21379  txnlly  21380  txtube  21383  txcmplem1  21384  txcmplem2  21385  xkococnlem  21402  basqtop  21454  tgqtop  21455  infil  21607  fmfnfmlem4  21701  hauspwpwf1  21731  tgpconncompss  21857  ustfilxp  21956  metrest  22269  tgioo  22539  zdis  22559  icccmplem1  22565  icccmplem2  22566  reconnlem2  22570  xrge0tsms  22577  cnheibor  22694  cnllycmp  22695  ncvs1  22897  cphsqrtcl  22924  cmetcaulem  23026  ovollb2lem  23196  ovolctb  23198  ovolshftlem1  23217  ovolscalem1  23221  ovolicc1  23224  ioombl1lem1  23266  ioorf  23281  ioorcl  23285  dyadf  23299  vitalilem2  23318  vitali  23322  i1faddlem  23400  dvres2lem  23614  dvaddbr  23641  dvmulbr  23642  lhop1lem  23714  lhop  23717  dvcnvrelem2  23719  ig1peu  23869  tayl0  24054  rlimcnp2  24627  xrlimcnp  24629  ppisval  24764  ppisval2  24765  ppinprm  24812  chtnprm  24814  2sqlem7  25083  chebbnd1lem1  25092  footex  25547  foot  25548  footne  25549  perprag  25552  colperpexlem3  25558  mideulem2  25560  lnopp2hpgb  25589  colopp  25595  lmieu  25610  lmimid  25620  hypcgrlem1  25625  hypcgrlem2  25626  trgcopyeulem  25631  f1otrg  25685  eengtrkg  25799  wlkres  26470  shuni  28047  5oalem1  28401  5oalem2  28402  5oalem4  28404  5oalem5  28405  3oalem2  28410  pjclem4  28946  pj3si  28954  xrge0tsmsd  29612  cmpcref  29741  cmppcmp  29749  dispcmp  29750  prsdm  29784  prsrn  29785  pnfneige0  29821  qqhucn  29860  rrhqima  29882  gsumesum  29944  esumcst  29948  esum2d  29978  sigainb  30022  inelpisys  30040  dynkin  30053  eulerpartlemgh  30263  eulerpartlemgs2  30265  eulerpartlemn  30266  sseqmw  30276  sseqf  30277  sseqp1  30280  fibp1  30286  bnj1379  30662  bnj1177  30835  cnllysconn  30988  rellysconn  30994  cvmsss2  31017  cvmcov2  31018  cvmopnlem  31021  mclsind  31228  poimirlem30  33110  blbnd  33257  ssbnd  33258  heiborlem1  33281  heiborlem8  33288  heibor  33291  mndomgmid  33341  pmodlem1  34651  pclfinN  34705  mapdunirnN  36458  hdmaprnlem9N  36668  elrfi  36776  elrfirn  36777  fnwe2lem2  37140  dfac11  37151  kelac1  37152  kelac2lem  37153  dfac21  37155  islssfgi  37161  filnm  37179  lpirlnr  37207  hbtlem6  37219  hbt  37220  cntzsdrg  37292  iocinico  37317  restuni3  38826  disjinfi  38889  fvelimad  38968  fnfvimad  38969  iooabslt  39167  iocopn  39192  icoopn  39197  uzinico  39233  limciccioolb  39289  limcicciooub  39305  islpcn  39307  limcresioolb  39311  limcleqr  39312  limsuppnfdlem  39369  ioccncflimc  39433  icccncfext  39435  icocncflimc  39437  cncfiooicclem1  39441  itgiccshift  39533  itgperiod  39534  itgsbtaddcnst  39535  stoweidlem57  39611  fourierdlem20  39681  fourierdlem32  39693  fourierdlem33  39694  fourierdlem48  39708  fourierdlem49  39709  fourierdlem62  39722  fourierdlem71  39731  fouriersw  39785  qndenserrnbllem  39851  qndenserrn  39856  salgencntex  39898  fsumlesge0  39931  sge0tsms  39934  sge0cl  39935  sge0f1o  39936  sge0sup  39945  sge0resplit  39960  sge0iunmptlemre  39969  sge0fodjrnlem  39970  sge0rpcpnf  39975  sge0xaddlem1  39987  ovolval4lem2  40201  sssmf  40284  smflimlem3  40318  smfsuplem1  40354  zrinitorngc  41318  zrtermorngc  41319  zrzeroorngc  41320  irinitoringc  41387  zrtermoringc  41388  zrninitoringc  41389  nzerooringczr  41390
  Copyright terms: Public domain W3C validator