Theorem elind 4166

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

Step	Hyp	Ref	Expression
1		elind.1	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
2		elind.2	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		elin 3933	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2109   ∩ cin 3916

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-ext 2702

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2709  df-cleq 2722  df-clel 2804  df-v 3452  df-in 3924

This theorem is referenced by:  fvelima2  6916  fvelimad  6931  fnfvimad  7211  tfrlem5  8351  uniinqs  8773  unifpw  9313  f1opwfi  9314  fissuni  9315  fipreima  9316  elfir  9373  inelfi  9376  cantnfcl  9627  frrlem15  9717  tskwe  9910  infpwfidom  9988  infpwfien  10022  ackbij2lem1  10178  ackbij1lem3  10181  ackbij1lem4  10182  ackbij1lem6  10184  ackbij1lem11  10189  fin23lem24  10282  isfin1-3  10346  fpwwe2lem11  10601  fpwwe  10606  canthnumlem  10608  fz1isolem  14433  isprm7  16685  setsstruct2  17151  strfv2d  17178  submre  17573  submrc  17596  isacs2  17621  coffth  17907  catcoppccl  18086  catcfuccl  18087  catcxpccl  18175  isdrs2  18274  fpwipodrs  18506  insubm  18752  sylow2a  19556  lsmmod  19612  lsmdisj  19618  lsmdisj2  19619  subgdisj1  19628  frgpnabllem1  19810  dmdprdd  19938  dprdfeq0  19961  dprdres  19967  dprddisj2  19978  dprd2da  19981  dmdprdsplit2lem  19984  ablfacrp  20005  pgpfac1lem3a  20015  pgpfac1lem3  20016  pgpfaclem1  20020  zrinitorngc  20558  zrtermorngc  20559  zrzeroorngc  20560  zrtermoringc  20591  zrninitoringc  20592  cntzsdrg  20718  2idl0  21177  2idl1  21178  zringlpirlem1  21379  zringlpirlem3  21381  irinitoringc  21396  nzerooringczr  21397  aspval  21789  mplind  21984  pmatcoe1fsupp  22595  baspartn  22848  bastg  22860  clsval2  22944  isopn3  22960  restbas  23052  lmss  23192  cmpcovf  23285  discmp  23292  cmpsublem  23293  cmpsub  23294  isconn2  23308  connclo  23309  llynlly  23371  restnlly  23376  restlly  23377  islly2  23378  llyrest  23379  nllyrest  23380  llyidm  23382  nllyidm  23383  hausllycmp  23388  cldllycmp  23389  lly1stc  23390  dislly  23391  llycmpkgen2  23444  1stckgenlem  23447  txlly  23530  txnlly  23531  txtube  23534  txcmplem1  23535  txcmplem2  23536  xkococnlem  23553  basqtop  23605  tgqtop  23606  infil  23757  fmfnfmlem4  23851  hauspwpwf1  23881  tgpconncompss  24008  ustfilxp  24107  metrest  24419  tgioo  24691  zdis  24712  icccmplem1  24718  icccmplem2  24719  reconnlem2  24723  xrge0tsms  24730  cnheibor  24861  cnllycmp  24862  ncvs1  25064  cphsqrtcl  25091  cmetcaulem  25195  ovollb2lem  25396  ovolctb  25398  ovolshftlem1  25417  ovolscalem1  25421  ovolicc1  25424  ioombl1lem1  25466  ioorf  25481  ioorcl  25485  dyadf  25499  vitalilem2  25517  vitali  25521  i1faddlem  25601  i1fmullem  25602  dvres2lem  25818  dvaddbr  25847  dvmulbr  25848  dvmulbrOLD  25849  lhop1lem  25925  lhop  25928  dvcnvrelem2  25930  ig1peu  26087  tayl0  26276  rlimcnp2  26883  xrlimcnp  26885  ppisval  27021  ppisval2  27022  ppinprm  27069  chtnprm  27071  2sqlem7  27342  chebbnd1lem1  27387  footexALT  28652  footexlem2  28654  foot  28656  footne  28657  perprag  28660  colperpexlem3  28666  mideulem2  28668  lnopp2hpgb  28697  colopp  28703  lmieu  28718  lmimid  28728  hypcgrlem1  28733  hypcgrlem2  28734  trgcopyeulem  28739  f1otrg  28805  eengtrkg  28920  shuni  31236  5oalem1  31590  5oalem2  31591  5oalem4  31593  5oalem5  31594  3oalem2  31599  pjclem4  32135  pj3si  32143  ccatf1  32877  xrge0tsmsd  33009  wrdpmtrlast  33057  idlinsubrg  33409  ssdifidlprm  33436  qsdrngilem  33472  qsdrngi  33473  pidufd  33521  exsslsb  33599  lindsunlem  33627  lbsdiflsp0  33629  dimkerim  33630  irngss  33689  cmpcref  33847  cmppcmp  33855  dispcmp  33856  zarcmplem  33878  prsdm  33911  prsrn  33912  pnfneige0  33948  qqhucn  33989  rrhqima  34011  gsumesum  34056  esumcst  34060  esum2d  34090  sigainb  34133  inelpisys  34151  dynkin  34164  eulerpartlemgh  34376  eulerpartlemgs2  34378  eulerpartlemn  34379  sseqmw  34389  sseqf  34390  sseqp1  34393  fibp1  34399  bnj1379  34827  bnj1177  35003  cnllysconn  35239  rellysconn  35245  cvmsss2  35268  cvmcov2  35269  cvmopnlem  35272  mclsind  35564  weiunfr  36462  poimirlem30  37651  blbnd  37788  ssbnd  37789  heiborlem1  37812  heiborlem8  37819  heibor  37822  mndomgmid  37872  pmodlem1  39847  pclfinN  39901  mapdunirnN  41651  hdmaprnlem9N  41858  mhpind  42589  elrfi  42689  elrfirn  42690  fnwe2lem2  43047  dfac11  43058  kelac1  43059  kelac2lem  43060  dfac21  43062  islssfgi  43068  filnm  43086  lpirlnr  43113  hbtlem6  43125  hbt  43126  iocinico  43208  restuni3  45119  disjinfi  45193  iooabslt  45504  iocopn  45525  icoopn  45530  uzinico  45564  limciccioolb  45626  limcicciooub  45642  islpcn  45644  limcresioolb  45648  limcleqr  45649  limsuppnfdlem  45706  limsupresxr  45771  liminfresxr  45772  liminfvalxr  45788  liminflelimsupuz  45790  cnrefiisplem  45834  ioccncflimc  45890  icccncfext  45892  icocncflimc  45894  cncfiooicclem1  45898  itgiccshift  45985  itgperiod  45986  itgsbtaddcnst  45987  stoweidlem57  46062  fourierdlem20  46132  fourierdlem32  46144  fourierdlem33  46145  fourierdlem48  46159  fourierdlem49  46160  fourierdlem62  46173  fourierdlem71  46182  fouriersw  46236  qndenserrnbllem  46299  qndenserrn  46304  salgencntex  46348  fsumlesge0  46382  sge0tsms  46385  sge0cl  46386  sge0f1o  46387  sge0sup  46396  sge0resplit  46411  sge0iunmptlemre  46420  sge0fodjrnlem  46421  sge0rpcpnf  46426  sge0xaddlem1  46438  ovolval4lem2  46655  sssmf  46743  smflimlem3  46778  smfsuplem1  46816  fcores  47072  prproropf1olem2  47509  iinfconstbaslem  49058  ffthoppf  49158  uobeqw  49212  uobeq  49213  swapfiso  49278  swapciso  49279  fucoppcffth  49404  thincciso  49446  thinccisod  49447  termcterm  49506  termcterm2  49507  termcterm3  49508  termcciso  49509  termc2  49511  diagciso  49532  diagcic  49533  uobeqterm  49539