Theorem elind 4163

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

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

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 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1543  df-ex 1780  df-sb 2066  df-clab 2708  df-cleq 2721  df-clel 2803  df-v 3449  df-in 3921

This theorem is referenced by:  fvelima2  6913  fvelimad  6928  fnfvimad  7208  tfrlem5  8348  uniinqs  8770  unifpw  9306  f1opwfi  9307  fissuni  9308  fipreima  9309  elfir  9366  inelfi  9369  cantnfcl  9620  frrlem15  9710  tskwe  9903  infpwfidom  9981  infpwfien  10015  ackbij2lem1  10171  ackbij1lem3  10174  ackbij1lem4  10175  ackbij1lem6  10177  ackbij1lem11  10182  fin23lem24  10275  isfin1-3  10339  fpwwe2lem11  10594  fpwwe  10599  canthnumlem  10601  fz1isolem  14426  isprm7  16678  setsstruct2  17144  strfv2d  17171  submre  17566  submrc  17589  isacs2  17614  coffth  17900  catcoppccl  18079  catcfuccl  18080  catcxpccl  18168  isdrs2  18267  fpwipodrs  18499  insubm  18745  sylow2a  19549  lsmmod  19605  lsmdisj  19611  lsmdisj2  19612  subgdisj1  19621  frgpnabllem1  19803  dmdprdd  19931  dprdfeq0  19954  dprdres  19960  dprddisj2  19971  dprd2da  19974  dmdprdsplit2lem  19977  ablfacrp  19998  pgpfac1lem3a  20008  pgpfac1lem3  20009  pgpfaclem1  20013  zrinitorngc  20551  zrtermorngc  20552  zrzeroorngc  20553  zrtermoringc  20584  zrninitoringc  20585  cntzsdrg  20711  2idl0  21170  2idl1  21171  zringlpirlem1  21372  zringlpirlem3  21374  irinitoringc  21389  nzerooringczr  21390  aspval  21782  mplind  21977  pmatcoe1fsupp  22588  baspartn  22841  bastg  22853  clsval2  22937  isopn3  22953  restbas  23045  lmss  23185  cmpcovf  23278  discmp  23285  cmpsublem  23286  cmpsub  23287  isconn2  23301  connclo  23302  llynlly  23364  restnlly  23369  restlly  23370  islly2  23371  llyrest  23372  nllyrest  23373  llyidm  23375  nllyidm  23376  hausllycmp  23381  cldllycmp  23382  lly1stc  23383  dislly  23384  llycmpkgen2  23437  1stckgenlem  23440  txlly  23523  txnlly  23524  txtube  23527  txcmplem1  23528  txcmplem2  23529  xkococnlem  23546  basqtop  23598  tgqtop  23599  infil  23750  fmfnfmlem4  23844  hauspwpwf1  23874  tgpconncompss  24001  ustfilxp  24100  metrest  24412  tgioo  24684  zdis  24705  icccmplem1  24711  icccmplem2  24712  reconnlem2  24716  xrge0tsms  24723  cnheibor  24854  cnllycmp  24855  ncvs1  25057  cphsqrtcl  25084  cmetcaulem  25188  ovollb2lem  25389  ovolctb  25391  ovolshftlem1  25410  ovolscalem1  25414  ovolicc1  25417  ioombl1lem1  25459  ioorf  25474  ioorcl  25478  dyadf  25492  vitalilem2  25510  vitali  25514  i1faddlem  25594  i1fmullem  25595  dvres2lem  25811  dvaddbr  25840  dvmulbr  25841  dvmulbrOLD  25842  lhop1lem  25918  lhop  25921  dvcnvrelem2  25923  ig1peu  26080  tayl0  26269  rlimcnp2  26876  xrlimcnp  26878  ppisval  27014  ppisval2  27015  ppinprm  27062  chtnprm  27064  2sqlem7  27335  chebbnd1lem1  27380  footexALT  28645  footexlem2  28647  foot  28649  footne  28650  perprag  28653  colperpexlem3  28659  mideulem2  28661  lnopp2hpgb  28690  colopp  28696  lmieu  28711  lmimid  28721  hypcgrlem1  28726  hypcgrlem2  28727  trgcopyeulem  28732  f1otrg  28798  eengtrkg  28913  shuni  31229  5oalem1  31583  5oalem2  31584  5oalem4  31586  5oalem5  31587  3oalem2  31592  pjclem4  32128  pj3si  32136  ccatf1  32870  xrge0tsmsd  33002  wrdpmtrlast  33050  idlinsubrg  33402  ssdifidlprm  33429  qsdrngilem  33465  qsdrngi  33466  pidufd  33514  exsslsb  33592  lindsunlem  33620  lbsdiflsp0  33622  dimkerim  33623  irngss  33682  cmpcref  33840  cmppcmp  33848  dispcmp  33849  zarcmplem  33871  prsdm  33904  prsrn  33905  pnfneige0  33941  qqhucn  33982  rrhqima  34004  gsumesum  34049  esumcst  34053  esum2d  34083  sigainb  34126  inelpisys  34144  dynkin  34157  eulerpartlemgh  34369  eulerpartlemgs2  34371  eulerpartlemn  34372  sseqmw  34382  sseqf  34383  sseqp1  34386  fibp1  34392  bnj1379  34820  bnj1177  34996  cnllysconn  35232  rellysconn  35238  cvmsss2  35261  cvmcov2  35262  cvmopnlem  35265  mclsind  35557  weiunfr  36455  poimirlem30  37644  blbnd  37781  ssbnd  37782  heiborlem1  37805  heiborlem8  37812  heibor  37815  mndomgmid  37865  pmodlem1  39840  pclfinN  39894  mapdunirnN  41644  hdmaprnlem9N  41851  mhpind  42582  elrfi  42682  elrfirn  42683  fnwe2lem2  43040  dfac11  43051  kelac1  43052  kelac2lem  43053  dfac21  43055  islssfgi  43061  filnm  43079  lpirlnr  43106  hbtlem6  43118  hbt  43119  iocinico  43201  restuni3  45112  disjinfi  45186  iooabslt  45497  iocopn  45518  icoopn  45523  uzinico  45557  limciccioolb  45619  limcicciooub  45635  islpcn  45637  limcresioolb  45641  limcleqr  45642  limsuppnfdlem  45699  limsupresxr  45764  liminfresxr  45765  liminfvalxr  45781  liminflelimsupuz  45783  cnrefiisplem  45827  ioccncflimc  45883  icccncfext  45885  icocncflimc  45887  cncfiooicclem1  45891  itgiccshift  45978  itgperiod  45979  itgsbtaddcnst  45980  stoweidlem57  46055  fourierdlem20  46125  fourierdlem32  46137  fourierdlem33  46138  fourierdlem48  46152  fourierdlem49  46153  fourierdlem62  46166  fourierdlem71  46175  fouriersw  46229  qndenserrnbllem  46292  qndenserrn  46297  salgencntex  46341  fsumlesge0  46375  sge0tsms  46378  sge0cl  46379  sge0f1o  46380  sge0sup  46389  sge0resplit  46404  sge0iunmptlemre  46413  sge0fodjrnlem  46414  sge0rpcpnf  46419  sge0xaddlem1  46431  ovolval4lem2  46648  sssmf  46736  smflimlem3  46771  smfsuplem1  46809  fcores  47068  prproropf1olem2  47505  iinfconstbaslem  49054  ffthoppf  49154  uobeqw  49208  uobeq  49209  swapfiso  49274  swapciso  49275  fucoppcffth  49400  thincciso  49442  thinccisod  49443  termcterm  49502  termcterm2  49503  termcterm3  49504  termcciso  49505  termc2  49507  diagciso  49528  diagcic  49529  uobeqterm  49535