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

Theorem elind 3790
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 3788 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 697 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1988  cin 3566
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
This theorem is referenced by:  tfrlem5  7461  uniinqs  7812  unifpw  8254  f1opwfi  8255  fissuni  8256  fipreima  8257  elfir  8306  inelfi  8309  cantnfcl  8549  tskwe  8761  infpwfidom  8836  infpwfien  8870  ackbij2lem1  9026  ackbij1lem3  9029  ackbij1lem4  9030  ackbij1lem6  9032  ackbij1lem11  9037  fin23lem24  9129  isfin1-3  9193  fpwwe2lem12  9448  fpwwe  9453  canthnumlem  9455  fz1isolem  13228  isprm7  15401  setsstruct2  15877  strfv2d  15886  submre  16246  submrc  16269  isacs2  16295  coffth  16577  catcoppccl  16739  catcfuccl  16740  catcxpccl  16828  isdrs2  16920  fpwipodrs  17145  sylow2a  18015  lsmmod  18069  lsmdisj  18075  lsmdisj2  18076  subgdisj1  18085  frgpnabllem1  18257  dmdprdd  18379  dprdfeq0  18402  dprdres  18408  dprddisj2  18419  dprd2da  18422  dmdprdsplit2lem  18425  ablfacrp  18446  pgpfac1lem3a  18456  pgpfac1lem3  18457  pgpfaclem1  18461  aspval  19309  mplind  19483  zringlpirlem1  19813  zringlpirlem3  19815  pmatcoe1fsupp  20487  baspartn  20739  bastg  20751  clsval2  20835  isopn3  20851  restbas  20943  lmss  21083  cmpcovf  21175  discmp  21182  cmpsublem  21183  cmpsub  21184  isconn2  21198  connclo  21199  llynlly  21261  restnlly  21266  restlly  21267  islly2  21268  llyrest  21269  nllyrest  21270  llyidm  21272  nllyidm  21273  hausllycmp  21278  cldllycmp  21279  lly1stc  21280  dislly  21281  llycmpkgen2  21334  1stckgenlem  21337  txlly  21420  txnlly  21421  txtube  21424  txcmplem1  21425  txcmplem2  21426  xkococnlem  21443  basqtop  21495  tgqtop  21496  infil  21648  fmfnfmlem4  21742  hauspwpwf1  21772  tgpconncompss  21898  ustfilxp  21997  metrest  22310  tgioo  22580  zdis  22600  icccmplem1  22606  icccmplem2  22607  reconnlem2  22611  xrge0tsms  22618  cnheibor  22735  cnllycmp  22736  ncvs1  22938  cphsqrtcl  22965  cmetcaulem  23067  ovollb2lem  23237  ovolctb  23239  ovolshftlem1  23258  ovolscalem1  23262  ovolicc1  23265  ioombl1lem1  23307  ioorf  23322  ioorcl  23326  dyadf  23340  vitalilem2  23359  vitali  23363  i1faddlem  23441  dvres2lem  23655  dvaddbr  23682  dvmulbr  23683  lhop1lem  23757  lhop  23760  dvcnvrelem2  23762  ig1peu  23912  tayl0  24097  rlimcnp2  24674  xrlimcnp  24676  ppisval  24811  ppisval2  24812  ppinprm  24859  chtnprm  24861  2sqlem7  25130  chebbnd1lem1  25139  footex  25594  foot  25595  footne  25596  perprag  25599  colperpexlem3  25605  mideulem2  25607  lnopp2hpgb  25636  colopp  25642  lmieu  25657  lmimid  25667  hypcgrlem1  25672  hypcgrlem2  25673  trgcopyeulem  25678  f1otrg  25732  eengtrkg  25846  wlkres  26548  shuni  28129  5oalem1  28483  5oalem2  28484  5oalem4  28486  5oalem5  28487  3oalem2  28492  pjclem4  29028  pj3si  29036  xrge0tsmsd  29759  cmpcref  29891  cmppcmp  29899  dispcmp  29900  prsdm  29934  prsrn  29935  pnfneige0  29971  qqhucn  30010  rrhqima  30032  gsumesum  30095  esumcst  30099  esum2d  30129  sigainb  30173  inelpisys  30191  dynkin  30204  eulerpartlemgh  30414  eulerpartlemgs2  30416  eulerpartlemn  30417  sseqmw  30427  sseqf  30428  sseqp1  30431  fibp1  30437  bnj1379  30875  bnj1177  31048  cnllysconn  31201  rellysconn  31207  cvmsss2  31230  cvmcov2  31231  cvmopnlem  31234  mclsind  31441  poimirlem30  33410  blbnd  33557  ssbnd  33558  heiborlem1  33581  heiborlem8  33588  heibor  33591  mndomgmid  33641  pmodlem1  34951  pclfinN  35005  mapdunirnN  36758  hdmaprnlem9N  36968  elrfi  37076  elrfirn  37077  fnwe2lem2  37440  dfac11  37451  kelac1  37452  kelac2lem  37453  dfac21  37455  islssfgi  37461  filnm  37479  lpirlnr  37506  hbtlem6  37518  hbt  37519  cntzsdrg  37591  iocinico  37616  restuni3  39121  disjinfi  39196  fvelimad  39274  fnfvimad  39275  fvelima2  39291  fnfvima2  39294  iooabslt  39524  iocopn  39549  icoopn  39554  uzinico  39590  limciccioolb  39653  limcicciooub  39669  islpcn  39671  limcresioolb  39675  limcleqr  39676  limsuppnfdlem  39733  limsupresxr  39792  liminfresxr  39793  liminfvalxr  39809  liminflelimsupuz  39811  ioccncflimc  39861  icccncfext  39863  icocncflimc  39865  cncfiooicclem1  39869  itgiccshift  39959  itgperiod  39960  itgsbtaddcnst  39961  stoweidlem57  40037  fourierdlem20  40107  fourierdlem32  40119  fourierdlem33  40120  fourierdlem48  40134  fourierdlem49  40135  fourierdlem62  40148  fourierdlem71  40157  fouriersw  40211  qndenserrnbllem  40277  qndenserrn  40282  salgencntex  40324  fsumlesge0  40357  sge0tsms  40360  sge0cl  40361  sge0f1o  40362  sge0sup  40371  sge0resplit  40386  sge0iunmptlemre  40395  sge0fodjrnlem  40396  sge0rpcpnf  40401  sge0xaddlem1  40413  ovolval4lem2  40627  sssmf  40710  smflimlem3  40744  smfsuplem1  40780  zrinitorngc  41765  zrtermorngc  41766  zrzeroorngc  41767  irinitoringc  41834  zrtermoringc  41835  zrninitoringc  41836  nzerooringczr  41837
  Copyright terms: Public domain W3C validator