Theorem elind 4129

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3887

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2710

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1542  df-ex 1783  df-sb 2069  df-clab 2717  df-cleq 2731  df-clel 2817  df-v 3435  df-in 3895

This theorem is referenced by:  fvelimad  6845  fnfvimad  7119  tfrlem5  8220  uniinqs  8595  unifpw  9131  f1opwfi  9132  fissuni  9133  fipreima  9134  elfir  9183  inelfi  9186  cantnfcl  9434  frrlem15  9524  tskwe  9717  infpwfidom  9793  infpwfien  9827  ackbij2lem1  9984  ackbij1lem3  9987  ackbij1lem4  9988  ackbij1lem6  9990  ackbij1lem11  9995  fin23lem24  10087  isfin1-3  10151  fpwwe2lem11  10406  fpwwe  10411  canthnumlem  10413  fz1isolem  14184  isprm7  16422  setsstruct2  16884  strfv2d  16912  submre  17323  submrc  17346  isacs2  17371  coffth  17661  catcoppccl  17841  catcoppcclOLD  17842  catcfuccl  17843  catcfucclOLD  17844  catcxpccl  17933  catcxpcclOLD  17934  isdrs2  18033  fpwipodrs  18267  insubm  18466  sylow2a  19233  lsmmod  19290  lsmdisj  19296  lsmdisj2  19297  subgdisj1  19306  frgpnabllem1  19483  dmdprdd  19611  dprdfeq0  19634  dprdres  19640  dprddisj2  19651  dprd2da  19654  dmdprdsplit2lem  19657  ablfacrp  19678  pgpfac1lem3a  19688  pgpfac1lem3  19689  pgpfaclem1  19693  cntzsdrg  20079  zringlpirlem1  20693  zringlpirlem3  20695  aspval  21086  mplind  21287  pmatcoe1fsupp  21859  baspartn  22113  bastg  22125  clsval2  22210  isopn3  22226  restbas  22318  lmss  22458  cmpcovf  22551  discmp  22558  cmpsublem  22559  cmpsub  22560  isconn2  22574  connclo  22575  llynlly  22637  restnlly  22642  restlly  22643  islly2  22644  llyrest  22645  nllyrest  22646  llyidm  22648  nllyidm  22649  hausllycmp  22654  cldllycmp  22655  lly1stc  22656  dislly  22657  llycmpkgen2  22710  1stckgenlem  22713  txlly  22796  txnlly  22797  txtube  22800  txcmplem1  22801  txcmplem2  22802  xkococnlem  22819  basqtop  22871  tgqtop  22872  infil  23023  fmfnfmlem4  23117  hauspwpwf1  23147  tgpconncompss  23274  ustfilxp  23373  metrest  23689  tgioo  23968  zdis  23988  icccmplem1  23994  icccmplem2  23995  reconnlem2  23999  xrge0tsms  24006  cnheibor  24127  cnllycmp  24128  ncvs1  24330  cphsqrtcl  24357  cmetcaulem  24461  ovollb2lem  24661  ovolctb  24663  ovolshftlem1  24682  ovolscalem1  24686  ovolicc1  24689  ioombl1lem1  24731  ioorf  24746  ioorcl  24750  dyadf  24764  vitalilem2  24782  vitali  24786  i1faddlem  24866  i1fmullem  24867  dvres2lem  25083  dvaddbr  25111  dvmulbr  25112  lhop1lem  25186  lhop  25189  dvcnvrelem2  25191  ig1peu  25345  tayl0  25530  rlimcnp2  26125  xrlimcnp  26127  ppisval  26262  ppisval2  26263  ppinprm  26310  chtnprm  26312  2sqlem7  26581  chebbnd1lem1  26626  footexALT  27088  footexlem2  27090  foot  27092  footne  27093  perprag  27096  colperpexlem3  27102  mideulem2  27104  lnopp2hpgb  27133  colopp  27139  lmieu  27154  lmimid  27164  hypcgrlem1  27169  hypcgrlem2  27170  trgcopyeulem  27175  f1otrg  27241  eengtrkg  27363  shuni  29671  5oalem1  30025  5oalem2  30026  5oalem4  30028  5oalem5  30029  3oalem2  30034  pjclem4  30570  pj3si  30578  ccatf1  31232  xrge0tsmsd  31326  idlinsubrg  31617  lindsunlem  31714  lbsdiflsp0  31716  dimkerim  31717  cmpcref  31809  cmppcmp  31817  dispcmp  31818  zarcmplem  31840  prsdm  31873  prsrn  31874  pnfneige0  31910  qqhucn  31951  rrhqima  31973  gsumesum  32036  esumcst  32040  esum2d  32070  sigainb  32113  inelpisys  32131  dynkin  32144  eulerpartlemgh  32354  eulerpartlemgs2  32356  eulerpartlemn  32357  sseqmw  32367  sseqf  32368  sseqp1  32371  fibp1  32377  bnj1379  32819  bnj1177  32995  cnllysconn  33216  rellysconn  33222  cvmsss2  33245  cvmcov2  33246  cvmopnlem  33249  mclsind  33541  poimirlem30  35816  blbnd  35954  ssbnd  35955  heiborlem1  35978  heiborlem8  35985  heibor  35988  mndomgmid  36038  pmodlem1  37867  pclfinN  37921  mapdunirnN  39671  hdmaprnlem9N  39878  mhpind  40290  prjcrv0  40477  elrfi  40523  elrfirn  40524  fnwe2lem2  40883  dfac11  40894  kelac1  40895  kelac2lem  40896  dfac21  40898  islssfgi  40904  filnm  40922  lpirlnr  40949  hbtlem6  40961  hbt  40962  iocinico  41050  restuni3  42674  disjinfi  42738  fvelima2  42813  iooabslt  43044  iocopn  43065  icoopn  43070  uzinico  43105  limciccioolb  43169  limcicciooub  43185  islpcn  43187  limcresioolb  43191  limcleqr  43192  limsuppnfdlem  43249  limsupresxr  43314  liminfresxr  43315  liminfvalxr  43331  liminflelimsupuz  43333  cnrefiisplem  43377  ioccncflimc  43433  icccncfext  43435  icocncflimc  43437  cncfiooicclem1  43441  itgiccshift  43528  itgperiod  43529  itgsbtaddcnst  43530  stoweidlem57  43605  fourierdlem20  43675  fourierdlem32  43687  fourierdlem33  43688  fourierdlem48  43702  fourierdlem49  43703  fourierdlem62  43716  fourierdlem71  43725  fouriersw  43779  qndenserrnbllem  43842  qndenserrn  43847  salgencntex  43889  fsumlesge0  43922  sge0tsms  43925  sge0cl  43926  sge0f1o  43927  sge0sup  43936  sge0resplit  43951  sge0iunmptlemre  43960  sge0fodjrnlem  43961  sge0rpcpnf  43966  sge0xaddlem1  43978  ovolval4lem2  44195  sssmf  44283  smflimlem3  44318  smfsuplem1  44355  fcores  44572  prproropf1olem2  44967  zrinitorngc  45569  zrtermorngc  45570  zrzeroorngc  45571  irinitoringc  45638  zrtermoringc  45639  zrninitoringc  45640  nzerooringczr  45641  thincciso  46341