Theorem elind 4151

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

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

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 3438  df-in 3910

This theorem is referenced by:  fvelima2  6875  fvelimad  6890  fnfvimad  7170  tfrlem5  8302  uniinqs  8724  unifpw  9245  f1opwfi  9246  fissuni  9247  fipreima  9248  elfir  9305  inelfi  9308  cantnfcl  9563  frrlem15  9653  tskwe  9846  infpwfidom  9922  infpwfien  9956  ackbij2lem1  10112  ackbij1lem3  10115  ackbij1lem4  10116  ackbij1lem6  10118  ackbij1lem11  10123  fin23lem24  10216  isfin1-3  10280  fpwwe2lem11  10535  fpwwe  10540  canthnumlem  10542  fz1isolem  14368  isprm7  16619  setsstruct2  17085  strfv2d  17112  submre  17507  submrc  17534  isacs2  17559  coffth  17845  catcoppccl  18024  catcfuccl  18025  catcxpccl  18113  isdrs2  18212  fpwipodrs  18446  insubm  18692  sylow2a  19498  lsmmod  19554  lsmdisj  19560  lsmdisj2  19561  subgdisj1  19570  frgpnabllem1  19752  dmdprdd  19880  dprdfeq0  19903  dprdres  19909  dprddisj2  19920  dprd2da  19923  dmdprdsplit2lem  19926  ablfacrp  19947  pgpfac1lem3a  19957  pgpfac1lem3  19958  pgpfaclem1  19962  zrinitorngc  20527  zrtermorngc  20528  zrzeroorngc  20529  zrtermoringc  20560  zrninitoringc  20561  cntzsdrg  20687  2idl0  21167  2idl1  21168  zringlpirlem1  21369  zringlpirlem3  21371  irinitoringc  21386  nzerooringczr  21387  aspval  21780  mplind  21975  pmatcoe1fsupp  22586  baspartn  22839  bastg  22851  clsval2  22935  isopn3  22951  restbas  23043  lmss  23183  cmpcovf  23276  discmp  23283  cmpsublem  23284  cmpsub  23285  isconn2  23299  connclo  23300  llynlly  23362  restnlly  23367  restlly  23368  islly2  23369  llyrest  23370  nllyrest  23371  llyidm  23373  nllyidm  23374  hausllycmp  23379  cldllycmp  23380  lly1stc  23381  dislly  23382  llycmpkgen2  23435  1stckgenlem  23438  txlly  23521  txnlly  23522  txtube  23525  txcmplem1  23526  txcmplem2  23527  xkococnlem  23544  basqtop  23596  tgqtop  23597  infil  23748  fmfnfmlem4  23842  hauspwpwf1  23872  tgpconncompss  23999  ustfilxp  24098  metrest  24410  tgioo  24682  zdis  24703  icccmplem1  24709  icccmplem2  24710  reconnlem2  24714  xrge0tsms  24721  cnheibor  24852  cnllycmp  24853  ncvs1  25055  cphsqrtcl  25082  cmetcaulem  25186  ovollb2lem  25387  ovolctb  25389  ovolshftlem1  25408  ovolscalem1  25412  ovolicc1  25415  ioombl1lem1  25457  ioorf  25472  ioorcl  25476  dyadf  25490  vitalilem2  25508  vitali  25512  i1faddlem  25592  i1fmullem  25593  dvres2lem  25809  dvaddbr  25838  dvmulbr  25839  dvmulbrOLD  25840  lhop1lem  25916  lhop  25919  dvcnvrelem2  25921  ig1peu  26078  tayl0  26267  rlimcnp2  26874  xrlimcnp  26876  ppisval  27012  ppisval2  27013  ppinprm  27060  chtnprm  27062  2sqlem7  27333  chebbnd1lem1  27378  footexALT  28663  footexlem2  28665  foot  28667  footne  28668  perprag  28671  colperpexlem3  28677  mideulem2  28679  lnopp2hpgb  28708  colopp  28714  lmieu  28729  lmimid  28739  hypcgrlem1  28744  hypcgrlem2  28745  trgcopyeulem  28750  f1otrg  28816  eengtrkg  28931  shuni  31244  5oalem1  31598  5oalem2  31599  5oalem4  31601  5oalem5  31602  3oalem2  31607  pjclem4  32143  pj3si  32151  ccatf1  32890  xrge0tsmsd  33015  wrdpmtrlast  33035  idlinsubrg  33368  ssdifidlprm  33395  qsdrngilem  33431  qsdrngi  33432  pidufd  33480  exsslsb  33563  lindsunlem  33591  lbsdiflsp0  33593  dimkerim  33594  irngss  33654  cmpcref  33817  cmppcmp  33825  dispcmp  33826  zarcmplem  33848  prsdm  33881  prsrn  33882  pnfneige0  33918  qqhucn  33959  rrhqima  33981  gsumesum  34026  esumcst  34030  esum2d  34060  sigainb  34103  inelpisys  34121  dynkin  34134  eulerpartlemgh  34346  eulerpartlemgs2  34348  eulerpartlemn  34349  sseqmw  34359  sseqf  34360  sseqp1  34363  fibp1  34369  bnj1379  34797  bnj1177  34973  cnllysconn  35218  rellysconn  35224  cvmsss2  35247  cvmcov2  35248  cvmopnlem  35251  mclsind  35543  weiunfr  36441  poimirlem30  37630  blbnd  37767  ssbnd  37768  heiborlem1  37791  heiborlem8  37798  heibor  37801  mndomgmid  37851  pmodlem1  39825  pclfinN  39879  mapdunirnN  41629  hdmaprnlem9N  41836  mhpind  42567  elrfi  42667  elrfirn  42668  fnwe2lem2  43024  dfac11  43035  kelac1  43036  kelac2lem  43037  dfac21  43039  islssfgi  43045  filnm  43063  lpirlnr  43090  hbtlem6  43102  hbt  43103  iocinico  43185  restuni3  45096  disjinfi  45170  iooabslt  45480  iocopn  45501  icoopn  45506  uzinico  45540  limciccioolb  45602  limcicciooub  45618  islpcn  45620  limcresioolb  45624  limcleqr  45625  limsuppnfdlem  45682  limsupresxr  45747  liminfresxr  45748  liminfvalxr  45764  liminflelimsupuz  45766  cnrefiisplem  45810  ioccncflimc  45866  icccncfext  45868  icocncflimc  45870  cncfiooicclem1  45874  itgiccshift  45961  itgperiod  45962  itgsbtaddcnst  45963  stoweidlem57  46038  fourierdlem20  46108  fourierdlem32  46120  fourierdlem33  46121  fourierdlem48  46135  fourierdlem49  46136  fourierdlem62  46149  fourierdlem71  46158  fouriersw  46212  qndenserrnbllem  46275  qndenserrn  46280  salgencntex  46324  fsumlesge0  46358  sge0tsms  46361  sge0cl  46362  sge0f1o  46363  sge0sup  46372  sge0resplit  46387  sge0iunmptlemre  46396  sge0fodjrnlem  46397  sge0rpcpnf  46402  sge0xaddlem1  46414  ovolval4lem2  46631  sssmf  46719  smflimlem3  46754  smfsuplem1  46792  fcores  47051  prproropf1olem2  47488  iinfconstbaslem  49050  ffthoppf  49150  uobeqw  49204  uobeq  49205  swapfiso  49270  swapciso  49271  fucoppcffth  49396  thincciso  49438  thinccisod  49439  termcterm  49498  termcterm2  49499  termcterm3  49500  termcciso  49501  termc2  49503  diagciso  49524  diagcic  49525  uobeqterm  49531