Theorem elind 4209

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

Syntax hints:   → wi 4   ∈ wcel 2105   ∩ cin 3961

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1539  df-ex 1776  df-sb 2062  df-clab 2712  df-cleq 2726  df-clel 2813  df-v 3479  df-in 3969

This theorem is referenced by:  fvelimad  6975  fnfvimad  7253  tfrlem5  8418  uniinqs  8835  unifpw  9392  f1opwfi  9393  fissuni  9394  fipreima  9395  elfir  9452  inelfi  9455  cantnfcl  9704  frrlem15  9794  tskwe  9987  infpwfidom  10065  infpwfien  10099  ackbij2lem1  10255  ackbij1lem3  10258  ackbij1lem4  10259  ackbij1lem6  10261  ackbij1lem11  10266  fin23lem24  10359  isfin1-3  10423  fpwwe2lem11  10678  fpwwe  10683  canthnumlem  10685  fz1isolem  14496  isprm7  16741  setsstruct2  17207  strfv2d  17235  submre  17649  submrc  17672  isacs2  17697  coffth  17989  catcoppccl  18170  catcoppcclOLD  18171  catcfuccl  18172  catcfucclOLD  18173  catcxpccl  18262  catcxpcclOLD  18263  isdrs2  18363  fpwipodrs  18597  insubm  18843  sylow2a  19651  lsmmod  19707  lsmdisj  19713  lsmdisj2  19714  subgdisj1  19723  frgpnabllem1  19905  dmdprdd  20033  dprdfeq0  20056  dprdres  20062  dprddisj2  20073  dprd2da  20076  dmdprdsplit2lem  20079  ablfacrp  20100  pgpfac1lem3a  20110  pgpfac1lem3  20111  pgpfaclem1  20115  zrinitorngc  20658  zrtermorngc  20659  zrzeroorngc  20660  zrtermoringc  20691  zrninitoringc  20692  cntzsdrg  20819  2idl0  21287  2idl1  21288  zringlpirlem1  21490  zringlpirlem3  21492  irinitoringc  21507  nzerooringczr  21508  aspval  21910  mplind  22111  pmatcoe1fsupp  22722  baspartn  22976  bastg  22988  clsval2  23073  isopn3  23089  restbas  23181  lmss  23321  cmpcovf  23414  discmp  23421  cmpsublem  23422  cmpsub  23423  isconn2  23437  connclo  23438  llynlly  23500  restnlly  23505  restlly  23506  islly2  23507  llyrest  23508  nllyrest  23509  llyidm  23511  nllyidm  23512  hausllycmp  23517  cldllycmp  23518  lly1stc  23519  dislly  23520  llycmpkgen2  23573  1stckgenlem  23576  txlly  23659  txnlly  23660  txtube  23663  txcmplem1  23664  txcmplem2  23665  xkococnlem  23682  basqtop  23734  tgqtop  23735  infil  23886  fmfnfmlem4  23980  hauspwpwf1  24010  tgpconncompss  24137  ustfilxp  24236  metrest  24552  tgioo  24831  zdis  24851  icccmplem1  24857  icccmplem2  24858  reconnlem2  24862  xrge0tsms  24869  cnheibor  25000  cnllycmp  25001  ncvs1  25204  cphsqrtcl  25231  cmetcaulem  25335  ovollb2lem  25536  ovolctb  25538  ovolshftlem1  25557  ovolscalem1  25561  ovolicc1  25564  ioombl1lem1  25606  ioorf  25621  ioorcl  25625  dyadf  25639  vitalilem2  25657  vitali  25661  i1faddlem  25741  i1fmullem  25742  dvres2lem  25959  dvaddbr  25988  dvmulbr  25989  dvmulbrOLD  25990  lhop1lem  26066  lhop  26069  dvcnvrelem2  26071  ig1peu  26228  tayl0  26417  rlimcnp2  27023  xrlimcnp  27025  ppisval  27161  ppisval2  27162  ppinprm  27209  chtnprm  27211  2sqlem7  27482  chebbnd1lem1  27527  footexALT  28740  footexlem2  28742  foot  28744  footne  28745  perprag  28748  colperpexlem3  28754  mideulem2  28756  lnopp2hpgb  28785  colopp  28791  lmieu  28806  lmimid  28816  hypcgrlem1  28821  hypcgrlem2  28822  trgcopyeulem  28827  f1otrg  28893  eengtrkg  29015  shuni  31328  5oalem1  31682  5oalem2  31683  5oalem4  31685  5oalem5  31686  3oalem2  31691  pjclem4  32227  pj3si  32235  ccatf1  32917  xrge0tsmsd  33047  wrdpmtrlast  33095  idlinsubrg  33438  ssdifidlprm  33465  qsdrngilem  33501  qsdrngi  33502  pidufd  33550  lindsunlem  33651  lbsdiflsp0  33653  dimkerim  33654  irngss  33701  cmpcref  33810  cmppcmp  33818  dispcmp  33819  zarcmplem  33841  prsdm  33874  prsrn  33875  pnfneige0  33911  qqhucn  33954  rrhqima  33976  gsumesum  34039  esumcst  34043  esum2d  34073  sigainb  34116  inelpisys  34134  dynkin  34147  eulerpartlemgh  34359  eulerpartlemgs2  34361  eulerpartlemn  34362  sseqmw  34372  sseqf  34373  sseqp1  34376  fibp1  34382  bnj1379  34822  bnj1177  34998  cnllysconn  35229  rellysconn  35235  cvmsss2  35258  cvmcov2  35259  cvmopnlem  35262  mclsind  35554  weiunfr  36449  poimirlem30  37636  blbnd  37773  ssbnd  37774  heiborlem1  37797  heiborlem8  37804  heibor  37807  mndomgmid  37857  pmodlem1  39828  pclfinN  39882  mapdunirnN  41632  hdmaprnlem9N  41839  mhpind  42580  elrfi  42681  elrfirn  42682  fnwe2lem2  43039  dfac11  43050  kelac1  43051  kelac2lem  43052  dfac21  43054  islssfgi  43060  filnm  43078  lpirlnr  43105  hbtlem6  43117  hbt  43118  iocinico  43200  restuni3  45057  disjinfi  45134  fvelima2  45204  iooabslt  45451  iocopn  45472  icoopn  45477  uzinico  45512  limciccioolb  45576  limcicciooub  45592  islpcn  45594  limcresioolb  45598  limcleqr  45599  limsuppnfdlem  45656  limsupresxr  45721  liminfresxr  45722  liminfvalxr  45738  liminflelimsupuz  45740  cnrefiisplem  45784  ioccncflimc  45840  icccncfext  45842  icocncflimc  45844  cncfiooicclem1  45848  itgiccshift  45935  itgperiod  45936  itgsbtaddcnst  45937  stoweidlem57  46012  fourierdlem20  46082  fourierdlem32  46094  fourierdlem33  46095  fourierdlem48  46109  fourierdlem49  46110  fourierdlem62  46123  fourierdlem71  46132  fouriersw  46186  qndenserrnbllem  46249  qndenserrn  46254  salgencntex  46298  fsumlesge0  46332  sge0tsms  46335  sge0cl  46336  sge0f1o  46337  sge0sup  46346  sge0resplit  46361  sge0iunmptlemre  46370  sge0fodjrnlem  46371  sge0rpcpnf  46376  sge0xaddlem1  46388  ovolval4lem2  46605  sssmf  46693  smflimlem3  46728  smfsuplem1  46766  fcores  47016  prproropf1olem2  47428  thincciso  48848  thinccisod  48849