Theorem elind 4200

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 3967	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵))
4	1, 2, 3	sylanbrc 583	1 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3950

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 2007  ax-8 2110  ax-9 2118  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2065  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3482  df-in 3958

This theorem is referenced by:  fvelima2  6961  fvelimad  6976  fnfvimad  7254  tfrlem5  8420  uniinqs  8837  unifpw  9395  f1opwfi  9396  fissuni  9397  fipreima  9398  elfir  9455  inelfi  9458  cantnfcl  9707  frrlem15  9797  tskwe  9990  infpwfidom  10068  infpwfien  10102  ackbij2lem1  10258  ackbij1lem3  10261  ackbij1lem4  10262  ackbij1lem6  10264  ackbij1lem11  10269  fin23lem24  10362  isfin1-3  10426  fpwwe2lem11  10681  fpwwe  10686  canthnumlem  10688  fz1isolem  14500  isprm7  16745  setsstruct2  17211  strfv2d  17238  submre  17648  submrc  17671  isacs2  17696  coffth  17983  catcoppccl  18162  catcfuccl  18163  catcxpccl  18252  isdrs2  18352  fpwipodrs  18585  insubm  18831  sylow2a  19637  lsmmod  19693  lsmdisj  19699  lsmdisj2  19700  subgdisj1  19709  frgpnabllem1  19891  dmdprdd  20019  dprdfeq0  20042  dprdres  20048  dprddisj2  20059  dprd2da  20062  dmdprdsplit2lem  20065  ablfacrp  20086  pgpfac1lem3a  20096  pgpfac1lem3  20097  pgpfaclem1  20101  zrinitorngc  20642  zrtermorngc  20643  zrzeroorngc  20644  zrtermoringc  20675  zrninitoringc  20676  cntzsdrg  20803  2idl0  21270  2idl1  21271  zringlpirlem1  21473  zringlpirlem3  21475  irinitoringc  21490  nzerooringczr  21491  aspval  21893  mplind  22094  pmatcoe1fsupp  22707  baspartn  22961  bastg  22973  clsval2  23058  isopn3  23074  restbas  23166  lmss  23306  cmpcovf  23399  discmp  23406  cmpsublem  23407  cmpsub  23408  isconn2  23422  connclo  23423  llynlly  23485  restnlly  23490  restlly  23491  islly2  23492  llyrest  23493  nllyrest  23494  llyidm  23496  nllyidm  23497  hausllycmp  23502  cldllycmp  23503  lly1stc  23504  dislly  23505  llycmpkgen2  23558  1stckgenlem  23561  txlly  23644  txnlly  23645  txtube  23648  txcmplem1  23649  txcmplem2  23650  xkococnlem  23667  basqtop  23719  tgqtop  23720  infil  23871  fmfnfmlem4  23965  hauspwpwf1  23995  tgpconncompss  24122  ustfilxp  24221  metrest  24537  tgioo  24817  zdis  24838  icccmplem1  24844  icccmplem2  24845  reconnlem2  24849  xrge0tsms  24856  cnheibor  24987  cnllycmp  24988  ncvs1  25191  cphsqrtcl  25218  cmetcaulem  25322  ovollb2lem  25523  ovolctb  25525  ovolshftlem1  25544  ovolscalem1  25548  ovolicc1  25551  ioombl1lem1  25593  ioorf  25608  ioorcl  25612  dyadf  25626  vitalilem2  25644  vitali  25648  i1faddlem  25728  i1fmullem  25729  dvres2lem  25945  dvaddbr  25974  dvmulbr  25975  dvmulbrOLD  25976  lhop1lem  26052  lhop  26055  dvcnvrelem2  26057  ig1peu  26214  tayl0  26403  rlimcnp2  27009  xrlimcnp  27011  ppisval  27147  ppisval2  27148  ppinprm  27195  chtnprm  27197  2sqlem7  27468  chebbnd1lem1  27513  footexALT  28726  footexlem2  28728  foot  28730  footne  28731  perprag  28734  colperpexlem3  28740  mideulem2  28742  lnopp2hpgb  28771  colopp  28777  lmieu  28792  lmimid  28802  hypcgrlem1  28807  hypcgrlem2  28808  trgcopyeulem  28813  f1otrg  28879  eengtrkg  29001  shuni  31319  5oalem1  31673  5oalem2  31674  5oalem4  31676  5oalem5  31677  3oalem2  31682  pjclem4  32218  pj3si  32226  ccatf1  32933  xrge0tsmsd  33065  wrdpmtrlast  33113  idlinsubrg  33459  ssdifidlprm  33486  qsdrngilem  33522  qsdrngi  33523  pidufd  33571  exsslsb  33647  lindsunlem  33675  lbsdiflsp0  33677  dimkerim  33678  irngss  33737  cmpcref  33849  cmppcmp  33857  dispcmp  33858  zarcmplem  33880  prsdm  33913  prsrn  33914  pnfneige0  33950  qqhucn  33993  rrhqima  34015  gsumesum  34060  esumcst  34064  esum2d  34094  sigainb  34137  inelpisys  34155  dynkin  34168  eulerpartlemgh  34380  eulerpartlemgs2  34382  eulerpartlemn  34383  sseqmw  34393  sseqf  34394  sseqp1  34397  fibp1  34403  bnj1379  34844  bnj1177  35020  cnllysconn  35250  rellysconn  35256  cvmsss2  35279  cvmcov2  35280  cvmopnlem  35283  mclsind  35575  weiunfr  36468  poimirlem30  37657  blbnd  37794  ssbnd  37795  heiborlem1  37818  heiborlem8  37825  heibor  37828  mndomgmid  37878  pmodlem1  39848  pclfinN  39902  mapdunirnN  41652  hdmaprnlem9N  41859  mhpind  42604  elrfi  42705  elrfirn  42706  fnwe2lem2  43063  dfac11  43074  kelac1  43075  kelac2lem  43076  dfac21  43078  islssfgi  43084  filnm  43102  lpirlnr  43129  hbtlem6  43141  hbt  43142  iocinico  43224  restuni3  45123  disjinfi  45197  iooabslt  45512  iocopn  45533  icoopn  45538  uzinico  45573  limciccioolb  45636  limcicciooub  45652  islpcn  45654  limcresioolb  45658  limcleqr  45659  limsuppnfdlem  45716  limsupresxr  45781  liminfresxr  45782  liminfvalxr  45798  liminflelimsupuz  45800  cnrefiisplem  45844  ioccncflimc  45900  icccncfext  45902  icocncflimc  45904  cncfiooicclem1  45908  itgiccshift  45995  itgperiod  45996  itgsbtaddcnst  45997  stoweidlem57  46072  fourierdlem20  46142  fourierdlem32  46154  fourierdlem33  46155  fourierdlem48  46169  fourierdlem49  46170  fourierdlem62  46183  fourierdlem71  46192  fouriersw  46246  qndenserrnbllem  46309  qndenserrn  46314  salgencntex  46358  fsumlesge0  46392  sge0tsms  46395  sge0cl  46396  sge0f1o  46397  sge0sup  46406  sge0resplit  46421  sge0iunmptlemre  46430  sge0fodjrnlem  46431  sge0rpcpnf  46436  sge0xaddlem1  46448  ovolval4lem2  46665  sssmf  46753  smflimlem3  46788  smfsuplem1  46826  fcores  47079  prproropf1olem2  47491  swapfiso  48991  swapciso  48992  thincciso  49102  thinccisod  49103  termcterm  49145  termcterm2  49146  termcterm3  49147  termc2  49148