Theorem elind 4159

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

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

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 3446  df-in 3918

This theorem is referenced by:  fvelima2  6895  fvelimad  6910  fnfvimad  7190  tfrlem5  8325  uniinqs  8747  unifpw  9282  f1opwfi  9283  fissuni  9284  fipreima  9285  elfir  9342  inelfi  9345  cantnfcl  9596  frrlem15  9686  tskwe  9879  infpwfidom  9957  infpwfien  9991  ackbij2lem1  10147  ackbij1lem3  10150  ackbij1lem4  10151  ackbij1lem6  10153  ackbij1lem11  10158  fin23lem24  10251  isfin1-3  10315  fpwwe2lem11  10570  fpwwe  10575  canthnumlem  10577  fz1isolem  14402  isprm7  16654  setsstruct2  17120  strfv2d  17147  submre  17542  submrc  17565  isacs2  17590  coffth  17876  catcoppccl  18055  catcfuccl  18056  catcxpccl  18144  isdrs2  18243  fpwipodrs  18475  insubm  18721  sylow2a  19525  lsmmod  19581  lsmdisj  19587  lsmdisj2  19588  subgdisj1  19597  frgpnabllem1  19779  dmdprdd  19907  dprdfeq0  19930  dprdres  19936  dprddisj2  19947  dprd2da  19950  dmdprdsplit2lem  19953  ablfacrp  19974  pgpfac1lem3a  19984  pgpfac1lem3  19985  pgpfaclem1  19989  zrinitorngc  20527  zrtermorngc  20528  zrzeroorngc  20529  zrtermoringc  20560  zrninitoringc  20561  cntzsdrg  20687  2idl0  21146  2idl1  21147  zringlpirlem1  21348  zringlpirlem3  21350  irinitoringc  21365  nzerooringczr  21366  aspval  21758  mplind  21953  pmatcoe1fsupp  22564  baspartn  22817  bastg  22829  clsval2  22913  isopn3  22929  restbas  23021  lmss  23161  cmpcovf  23254  discmp  23261  cmpsublem  23262  cmpsub  23263  isconn2  23277  connclo  23278  llynlly  23340  restnlly  23345  restlly  23346  islly2  23347  llyrest  23348  nllyrest  23349  llyidm  23351  nllyidm  23352  hausllycmp  23357  cldllycmp  23358  lly1stc  23359  dislly  23360  llycmpkgen2  23413  1stckgenlem  23416  txlly  23499  txnlly  23500  txtube  23503  txcmplem1  23504  txcmplem2  23505  xkococnlem  23522  basqtop  23574  tgqtop  23575  infil  23726  fmfnfmlem4  23820  hauspwpwf1  23850  tgpconncompss  23977  ustfilxp  24076  metrest  24388  tgioo  24660  zdis  24681  icccmplem1  24687  icccmplem2  24688  reconnlem2  24692  xrge0tsms  24699  cnheibor  24830  cnllycmp  24831  ncvs1  25033  cphsqrtcl  25060  cmetcaulem  25164  ovollb2lem  25365  ovolctb  25367  ovolshftlem1  25386  ovolscalem1  25390  ovolicc1  25393  ioombl1lem1  25435  ioorf  25450  ioorcl  25454  dyadf  25468  vitalilem2  25486  vitali  25490  i1faddlem  25570  i1fmullem  25571  dvres2lem  25787  dvaddbr  25816  dvmulbr  25817  dvmulbrOLD  25818  lhop1lem  25894  lhop  25897  dvcnvrelem2  25899  ig1peu  26056  tayl0  26245  rlimcnp2  26852  xrlimcnp  26854  ppisval  26990  ppisval2  26991  ppinprm  27038  chtnprm  27040  2sqlem7  27311  chebbnd1lem1  27356  footexALT  28621  footexlem2  28623  foot  28625  footne  28626  perprag  28629  colperpexlem3  28635  mideulem2  28637  lnopp2hpgb  28666  colopp  28672  lmieu  28687  lmimid  28697  hypcgrlem1  28702  hypcgrlem2  28703  trgcopyeulem  28708  f1otrg  28774  eengtrkg  28889  shuni  31202  5oalem1  31556  5oalem2  31557  5oalem4  31559  5oalem5  31560  3oalem2  31565  pjclem4  32101  pj3si  32109  ccatf1  32843  xrge0tsmsd  32975  wrdpmtrlast  33023  idlinsubrg  33375  ssdifidlprm  33402  qsdrngilem  33438  qsdrngi  33439  pidufd  33487  exsslsb  33565  lindsunlem  33593  lbsdiflsp0  33595  dimkerim  33596  irngss  33655  cmpcref  33813  cmppcmp  33821  dispcmp  33822  zarcmplem  33844  prsdm  33877  prsrn  33878  pnfneige0  33914  qqhucn  33955  rrhqima  33977  gsumesum  34022  esumcst  34026  esum2d  34056  sigainb  34099  inelpisys  34117  dynkin  34130  eulerpartlemgh  34342  eulerpartlemgs2  34344  eulerpartlemn  34345  sseqmw  34355  sseqf  34356  sseqp1  34359  fibp1  34365  bnj1379  34793  bnj1177  34969  cnllysconn  35205  rellysconn  35211  cvmsss2  35234  cvmcov2  35235  cvmopnlem  35238  mclsind  35530  weiunfr  36428  poimirlem30  37617  blbnd  37754  ssbnd  37755  heiborlem1  37778  heiborlem8  37785  heibor  37788  mndomgmid  37838  pmodlem1  39813  pclfinN  39867  mapdunirnN  41617  hdmaprnlem9N  41824  mhpind  42555  elrfi  42655  elrfirn  42656  fnwe2lem2  43013  dfac11  43024  kelac1  43025  kelac2lem  43026  dfac21  43028  islssfgi  43034  filnm  43052  lpirlnr  43079  hbtlem6  43091  hbt  43092  iocinico  43174  restuni3  45085  disjinfi  45159  iooabslt  45470  iocopn  45491  icoopn  45496  uzinico  45530  limciccioolb  45592  limcicciooub  45608  islpcn  45610  limcresioolb  45614  limcleqr  45615  limsuppnfdlem  45672  limsupresxr  45737  liminfresxr  45738  liminfvalxr  45754  liminflelimsupuz  45756  cnrefiisplem  45800  ioccncflimc  45856  icccncfext  45858  icocncflimc  45860  cncfiooicclem1  45864  itgiccshift  45951  itgperiod  45952  itgsbtaddcnst  45953  stoweidlem57  46028  fourierdlem20  46098  fourierdlem32  46110  fourierdlem33  46111  fourierdlem48  46125  fourierdlem49  46126  fourierdlem62  46139  fourierdlem71  46148  fouriersw  46202  qndenserrnbllem  46265  qndenserrn  46270  salgencntex  46314  fsumlesge0  46348  sge0tsms  46351  sge0cl  46352  sge0f1o  46353  sge0sup  46362  sge0resplit  46377  sge0iunmptlemre  46386  sge0fodjrnlem  46387  sge0rpcpnf  46392  sge0xaddlem1  46404  ovolval4lem2  46621  sssmf  46709  smflimlem3  46744  smfsuplem1  46782  fcores  47041  prproropf1olem2  47478  iinfconstbaslem  49027  ffthoppf  49127  uobeqw  49181  uobeq  49182  swapfiso  49247  swapciso  49248  fucoppcffth  49373  thincciso  49415  thinccisod  49416  termcterm  49475  termcterm2  49476  termcterm3  49477  termcciso  49478  termc2  49480  diagciso  49501  diagcic  49502  uobeqterm  49508