Theorem elind 4124

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3882

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1799  ax-4 1813  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2110  ax-9 2118  ax-ext 2709

This theorem depends on definitions:  df-bi 206  df-an 396  df-tru 1542  df-ex 1784  df-sb 2069  df-clab 2716  df-cleq 2730  df-clel 2817  df-v 3424  df-in 3890

This theorem is referenced by:  fvelimad  6818  fnfvimad  7092  tfrlem5  8182  uniinqs  8544  unifpw  9052  f1opwfi  9053  fissuni  9054  fipreima  9055  elfir  9104  inelfi  9107  cantnfcl  9355  frrlem15  9446  tskwe  9639  infpwfidom  9715  infpwfien  9749  ackbij2lem1  9906  ackbij1lem3  9909  ackbij1lem4  9910  ackbij1lem6  9912  ackbij1lem11  9917  fin23lem24  10009  isfin1-3  10073  fpwwe2lem11  10328  fpwwe  10333  canthnumlem  10335  fz1isolem  14103  isprm7  16341  setsstruct2  16803  strfv2d  16831  submre  17231  submrc  17254  isacs2  17279  coffth  17568  catcoppccl  17748  catcoppcclOLD  17749  catcfuccl  17750  catcfucclOLD  17751  catcxpccl  17840  catcxpcclOLD  17841  isdrs2  17939  fpwipodrs  18173  insubm  18372  sylow2a  19139  lsmmod  19196  lsmdisj  19202  lsmdisj2  19203  subgdisj1  19212  frgpnabllem1  19389  dmdprdd  19517  dprdfeq0  19540  dprdres  19546  dprddisj2  19557  dprd2da  19560  dmdprdsplit2lem  19563  ablfacrp  19584  pgpfac1lem3a  19594  pgpfac1lem3  19595  pgpfaclem1  19599  cntzsdrg  19985  zringlpirlem1  20596  zringlpirlem3  20598  aspval  20987  mplind  21188  pmatcoe1fsupp  21758  baspartn  22012  bastg  22024  clsval2  22109  isopn3  22125  restbas  22217  lmss  22357  cmpcovf  22450  discmp  22457  cmpsublem  22458  cmpsub  22459  isconn2  22473  connclo  22474  llynlly  22536  restnlly  22541  restlly  22542  islly2  22543  llyrest  22544  nllyrest  22545  llyidm  22547  nllyidm  22548  hausllycmp  22553  cldllycmp  22554  lly1stc  22555  dislly  22556  llycmpkgen2  22609  1stckgenlem  22612  txlly  22695  txnlly  22696  txtube  22699  txcmplem1  22700  txcmplem2  22701  xkococnlem  22718  basqtop  22770  tgqtop  22771  infil  22922  fmfnfmlem4  23016  hauspwpwf1  23046  tgpconncompss  23173  ustfilxp  23272  metrest  23586  tgioo  23865  zdis  23885  icccmplem1  23891  icccmplem2  23892  reconnlem2  23896  xrge0tsms  23903  cnheibor  24024  cnllycmp  24025  ncvs1  24226  cphsqrtcl  24253  cmetcaulem  24357  ovollb2lem  24557  ovolctb  24559  ovolshftlem1  24578  ovolscalem1  24582  ovolicc1  24585  ioombl1lem1  24627  ioorf  24642  ioorcl  24646  dyadf  24660  vitalilem2  24678  vitali  24682  i1faddlem  24762  i1fmullem  24763  dvres2lem  24979  dvaddbr  25007  dvmulbr  25008  lhop1lem  25082  lhop  25085  dvcnvrelem2  25087  ig1peu  25241  tayl0  25426  rlimcnp2  26021  xrlimcnp  26023  ppisval  26158  ppisval2  26159  ppinprm  26206  chtnprm  26208  2sqlem7  26477  chebbnd1lem1  26522  footexALT  26983  footexlem2  26985  foot  26987  footne  26988  perprag  26991  colperpexlem3  26997  mideulem2  26999  lnopp2hpgb  27028  colopp  27034  lmieu  27049  lmimid  27059  hypcgrlem1  27064  hypcgrlem2  27065  trgcopyeulem  27070  f1otrg  27136  eengtrkg  27257  shuni  29563  5oalem1  29917  5oalem2  29918  5oalem4  29920  5oalem5  29921  3oalem2  29926  pjclem4  30462  pj3si  30470  ccatf1  31125  xrge0tsmsd  31219  idlinsubrg  31510  lindsunlem  31607  lbsdiflsp0  31609  dimkerim  31610  cmpcref  31702  cmppcmp  31710  dispcmp  31711  zarcmplem  31733  prsdm  31766  prsrn  31767  pnfneige0  31803  qqhucn  31842  rrhqima  31864  gsumesum  31927  esumcst  31931  esum2d  31961  sigainb  32004  inelpisys  32022  dynkin  32035  eulerpartlemgh  32245  eulerpartlemgs2  32247  eulerpartlemn  32248  sseqmw  32258  sseqf  32259  sseqp1  32262  fibp1  32268  bnj1379  32710  bnj1177  32886  cnllysconn  33107  rellysconn  33113  cvmsss2  33136  cvmcov2  33137  cvmopnlem  33140  mclsind  33432  poimirlem30  35734  blbnd  35872  ssbnd  35873  heiborlem1  35896  heiborlem8  35903  heibor  35906  mndomgmid  35956  pmodlem1  37787  pclfinN  37841  mapdunirnN  39591  hdmaprnlem9N  39798  mhpind  40206  elrfi  40432  elrfirn  40433  fnwe2lem2  40792  dfac11  40803  kelac1  40804  kelac2lem  40805  dfac21  40807  islssfgi  40813  filnm  40831  lpirlnr  40858  hbtlem6  40870  hbt  40871  iocinico  40959  restuni3  42556  disjinfi  42620  fvelima2  42695  iooabslt  42927  iocopn  42948  icoopn  42953  uzinico  42988  limciccioolb  43052  limcicciooub  43068  islpcn  43070  limcresioolb  43074  limcleqr  43075  limsuppnfdlem  43132  limsupresxr  43197  liminfresxr  43198  liminfvalxr  43214  liminflelimsupuz  43216  cnrefiisplem  43260  ioccncflimc  43316  icccncfext  43318  icocncflimc  43320  cncfiooicclem1  43324  itgiccshift  43411  itgperiod  43412  itgsbtaddcnst  43413  stoweidlem57  43488  fourierdlem20  43558  fourierdlem32  43570  fourierdlem33  43571  fourierdlem48  43585  fourierdlem49  43586  fourierdlem62  43599  fourierdlem71  43608  fouriersw  43662  qndenserrnbllem  43725  qndenserrn  43730  salgencntex  43772  fsumlesge0  43805  sge0tsms  43808  sge0cl  43809  sge0f1o  43810  sge0sup  43819  sge0resplit  43834  sge0iunmptlemre  43843  sge0fodjrnlem  43844  sge0rpcpnf  43849  sge0xaddlem1  43861  ovolval4lem2  44078  sssmf  44161  smflimlem3  44195  smfsuplem1  44231  fcores  44448  prproropf1olem2  44844  zrinitorngc  45446  zrtermorngc  45447  zrzeroorngc  45448  irinitoringc  45515  zrtermoringc  45516  zrninitoringc  45517  nzerooringczr  45518  thincciso  46218