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

Theorem elind 3759
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 3757 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 694 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1976  cin 3538
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
This theorem is referenced by:  tfrlem5  7340  uniinqs  7691  unifpw  8129  f1opwfi  8130  fissuni  8131  fipreima  8132  elfir  8181  inelfi  8184  cantnfcl  8424  tskwe  8636  infpwfidom  8711  infpwfien  8745  ackbij2lem1  8901  ackbij1lem3  8904  ackbij1lem4  8905  ackbij1lem6  8907  ackbij1lem11  8912  fin23lem24  9004  isfin1-3  9068  fpwwe2lem12  9319  fpwwe  9324  canthnumlem  9326  fz1isolem  13054  isprm7  15204  strfv2d  15679  submre  16034  submrc  16057  isacs2  16083  coffth  16365  catcoppccl  16527  catcfuccl  16528  catcxpccl  16616  isdrs2  16708  fpwipodrs  16933  sylow2a  17803  lsmmod  17857  lsmdisj  17863  lsmdisj2  17864  subgdisj1  17873  frgpnabllem1  18045  dmdprdd  18167  dprdfeq0  18190  dprdres  18196  dprddisj2  18207  dprd2da  18210  dmdprdsplit2lem  18213  ablfacrp  18234  pgpfac1lem3a  18244  pgpfac1lem3  18245  pgpfaclem1  18249  aspval  19095  mplind  19269  zringlpirlem1  19597  zringlpirlem3  19599  pmatcoe1fsupp  20267  baspartn  20511  bastg  20523  clsval2  20606  isopn3  20622  restbas  20714  lmss  20854  cmpcovf  20946  discmp  20953  cmpsublem  20954  cmpsub  20955  iscon2  20969  conclo  20970  llynlly  21032  restnlly  21037  restlly  21038  islly2  21039  llyrest  21040  nllyrest  21041  llyidm  21043  nllyidm  21044  hausllycmp  21049  cldllycmp  21050  lly1stc  21051  dislly  21052  llycmpkgen2  21105  1stckgenlem  21108  txlly  21191  txnlly  21192  txtube  21195  txcmplem1  21196  txcmplem2  21197  xkococnlem  21214  basqtop  21266  tgqtop  21267  infil  21419  fmfnfmlem4  21513  hauspwpwf1  21543  tgpconcompss  21669  ustfilxp  21768  metrest  22080  tgioo  22339  zdis  22359  icccmplem1  22365  icccmplem2  22366  reconnlem2  22370  xrge0tsms  22377  cnheibor  22493  cnllycmp  22494  ncvs1  22691  cphsqrtcl  22716  cmetcaulem  22812  ovollb2lem  22980  ovolctb  22982  ovolshftlem1  23001  ovolscalem1  23005  ovolicc1  23008  ioombl1lem1  23050  ioorf  23064  ioorcl  23068  dyadf  23082  vitalilem2  23101  vitali  23105  i1faddlem  23183  dvres2lem  23397  dvaddbr  23424  dvmulbr  23425  lhop1lem  23497  lhop  23500  dvcnvrelem2  23502  ig1peu  23652  tayl0  23837  rlimcnp2  24410  xrlimcnp  24412  ppisval  24547  ppisval2  24548  ppinprm  24595  chtnprm  24597  2sqlem7  24866  chebbnd1lem1  24875  footex  25331  foot  25332  footne  25333  perprag  25336  colperpexlem3  25342  mideulem2  25344  lnopp2hpgb  25373  colopp  25379  lmieu  25394  lmimid  25404  hypcgrlem1  25409  hypcgrlem2  25410  trgcopyeulem  25415  f1otrg  25469  eengtrkg  25583  shuni  27349  5oalem1  27703  5oalem2  27704  5oalem4  27706  5oalem5  27707  3oalem2  27712  pjclem4  28248  pj3si  28256  xrge0tsmsd  28922  cmpcref  29051  cmppcmp  29059  dispcmp  29060  prsdm  29094  prsrn  29095  pnfneige0  29131  qqhucn  29170  rrhqima  29192  gsumesum  29254  esumcst  29258  esum2d  29288  sigainb  29332  inelpisys  29350  dynkin  29363  eulerpartlemgh  29573  eulerpartlemgs2  29575  eulerpartlemn  29576  sseqmw  29586  sseqf  29587  sseqp1  29590  fibp1  29596  bnj1379  29961  bnj1177  30134  cnllyscon  30287  rellyscon  30293  cvmsss2  30316  cvmcov2  30317  cvmopnlem  30320  mclsind  30527  poimirlem30  32412  blbnd  32559  ssbnd  32560  heiborlem1  32583  heiborlem8  32590  heibor  32593  mndomgmid  32643  pmodlem1  33953  pclfinN  34007  mapdunirnN  35760  hdmaprnlem9N  35970  elrfi  36078  elrfirn  36079  fnwe2lem2  36442  dfac11  36453  kelac1  36454  kelac2lem  36455  dfac21  36457  islssfgi  36463  filnm  36481  lpirlnr  36509  hbtlem6  36521  hbt  36522  cntzsdrg  36594  iocinico  36619  restuni3  38136  disjinfi  38178  iooabslt  38372  iocopn  38397  icoopn  38402  limciccioolb  38492  limcicciooub  38508  islpcn  38510  limcresioolb  38514  limcleqr  38515  ioccncflimc  38575  icccncfext  38577  icocncflimc  38579  cncfiooicclem1  38583  itgiccshift  38676  itgperiod  38677  itgsbtaddcnst  38678  stoweidlem57  38754  fourierdlem20  38824  fourierdlem32  38836  fourierdlem33  38837  fourierdlem48  38851  fourierdlem49  38852  fourierdlem62  38865  fourierdlem71  38874  fouriersw  38928  qndenserrnbllem  38994  qndenserrn  38999  salgencntex  39041  fsumlesge0  39074  sge0tsms  39077  sge0cl  39078  sge0f1o  39079  sge0sup  39088  sge0resplit  39103  sge0iunmptlemre  39112  sge0fodjrnlem  39113  sge0rpcpnf  39118  sge0xaddlem1  39130  ovolval4lem2  39344  sssmf  39429  smflimlem3  39463  1wlkres  40881  zrinitorngc  41794  zrtermorngc  41795  zrzeroorngc  41796  irinitoringc  41863  zrtermoringc  41864  zrninitoringc  41865  nzerooringczr  41866
  Copyright terms: Public domain W3C validator