Theorem elind 4108

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

Syntax hints:   → wi 4   ∈ wcel 2110   ∩ cin 3865

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1803  ax-4 1817  ax-5 1918  ax-6 1976  ax-7 2016  ax-8 2112  ax-9 2120  ax-ext 2708

This theorem depends on definitions:  df-bi 210  df-an 400  df-tru 1546  df-ex 1788  df-sb 2071  df-clab 2715  df-cleq 2729  df-clel 2816  df-v 3410  df-in 3873

This theorem is referenced by:  fvelimad  6779  fnfvimad  7050  tfrlem5  8116  uniinqs  8479  unifpw  8979  f1opwfi  8980  fissuni  8981  fipreima  8982  elfir  9031  inelfi  9034  cantnfcl  9282  frrlem15  9373  tskwe  9566  infpwfidom  9642  infpwfien  9676  ackbij2lem1  9833  ackbij1lem3  9836  ackbij1lem4  9837  ackbij1lem6  9839  ackbij1lem11  9844  fin23lem24  9936  isfin1-3  10000  fpwwe2lem11  10255  fpwwe  10260  canthnumlem  10262  fz1isolem  14027  isprm7  16265  setsstruct2  16727  strfv2d  16752  submre  17108  submrc  17131  isacs2  17156  coffth  17443  catcoppccl  17623  catcoppcclOLD  17624  catcfuccl  17625  catcfucclOLD  17626  catcxpccl  17714  catcxpcclOLD  17715  isdrs2  17813  fpwipodrs  18046  insubm  18245  sylow2a  19008  lsmmod  19065  lsmdisj  19071  lsmdisj2  19072  subgdisj1  19081  frgpnabllem1  19258  dmdprdd  19386  dprdfeq0  19409  dprdres  19415  dprddisj2  19426  dprd2da  19429  dmdprdsplit2lem  19432  ablfacrp  19453  pgpfac1lem3a  19463  pgpfac1lem3  19464  pgpfaclem1  19468  cntzsdrg  19846  zringlpirlem1  20449  zringlpirlem3  20451  aspval  20832  mplind  21028  pmatcoe1fsupp  21598  baspartn  21851  bastg  21863  clsval2  21947  isopn3  21963  restbas  22055  lmss  22195  cmpcovf  22288  discmp  22295  cmpsublem  22296  cmpsub  22297  isconn2  22311  connclo  22312  llynlly  22374  restnlly  22379  restlly  22380  islly2  22381  llyrest  22382  nllyrest  22383  llyidm  22385  nllyidm  22386  hausllycmp  22391  cldllycmp  22392  lly1stc  22393  dislly  22394  llycmpkgen2  22447  1stckgenlem  22450  txlly  22533  txnlly  22534  txtube  22537  txcmplem1  22538  txcmplem2  22539  xkococnlem  22556  basqtop  22608  tgqtop  22609  infil  22760  fmfnfmlem4  22854  hauspwpwf1  22884  tgpconncompss  23011  ustfilxp  23110  metrest  23422  tgioo  23693  zdis  23713  icccmplem1  23719  icccmplem2  23720  reconnlem2  23724  xrge0tsms  23731  cnheibor  23852  cnllycmp  23853  ncvs1  24054  cphsqrtcl  24081  cmetcaulem  24185  ovollb2lem  24385  ovolctb  24387  ovolshftlem1  24406  ovolscalem1  24410  ovolicc1  24413  ioombl1lem1  24455  ioorf  24470  ioorcl  24474  dyadf  24488  vitalilem2  24506  vitali  24510  i1faddlem  24590  i1fmullem  24591  dvres2lem  24807  dvaddbr  24835  dvmulbr  24836  lhop1lem  24910  lhop  24913  dvcnvrelem2  24915  ig1peu  25069  tayl0  25254  rlimcnp2  25849  xrlimcnp  25851  ppisval  25986  ppisval2  25987  ppinprm  26034  chtnprm  26036  2sqlem7  26305  chebbnd1lem1  26350  footexALT  26809  footexlem2  26811  foot  26813  footne  26814  perprag  26817  colperpexlem3  26823  mideulem2  26825  lnopp2hpgb  26854  colopp  26860  lmieu  26875  lmimid  26885  hypcgrlem1  26890  hypcgrlem2  26891  trgcopyeulem  26896  f1otrg  26962  eengtrkg  27077  shuni  29381  5oalem1  29735  5oalem2  29736  5oalem4  29738  5oalem5  29739  3oalem2  29744  pjclem4  30280  pj3si  30288  ccatf1  30943  xrge0tsmsd  31036  idlinsubrg  31322  lindsunlem  31419  lbsdiflsp0  31421  dimkerim  31422  cmpcref  31514  cmppcmp  31522  dispcmp  31523  zarcmplem  31545  prsdm  31578  prsrn  31579  pnfneige0  31615  qqhucn  31654  rrhqima  31676  gsumesum  31739  esumcst  31743  esum2d  31773  sigainb  31816  inelpisys  31834  dynkin  31847  eulerpartlemgh  32057  eulerpartlemgs2  32059  eulerpartlemn  32060  sseqmw  32070  sseqf  32071  sseqp1  32074  fibp1  32080  bnj1379  32523  bnj1177  32699  cnllysconn  32920  rellysconn  32926  cvmsss2  32949  cvmcov2  32950  cvmopnlem  32953  mclsind  33245  poimirlem30  35544  blbnd  35682  ssbnd  35683  heiborlem1  35706  heiborlem8  35713  heibor  35716  mndomgmid  35766  pmodlem1  37597  pclfinN  37651  mapdunirnN  39401  hdmaprnlem9N  39608  mhpind  39993  elrfi  40219  elrfirn  40220  fnwe2lem2  40579  dfac11  40590  kelac1  40591  kelac2lem  40592  dfac21  40594  islssfgi  40600  filnm  40618  lpirlnr  40645  hbtlem6  40657  hbt  40658  iocinico  40746  restuni3  42340  disjinfi  42404  fvelima2  42478  iooabslt  42712  iocopn  42733  icoopn  42738  uzinico  42773  limciccioolb  42837  limcicciooub  42853  islpcn  42855  limcresioolb  42859  limcleqr  42860  limsuppnfdlem  42917  limsupresxr  42982  liminfresxr  42983  liminfvalxr  42999  liminflelimsupuz  43001  cnrefiisplem  43045  ioccncflimc  43101  icccncfext  43103  icocncflimc  43105  cncfiooicclem1  43109  itgiccshift  43196  itgperiod  43197  itgsbtaddcnst  43198  stoweidlem57  43273  fourierdlem20  43343  fourierdlem32  43355  fourierdlem33  43356  fourierdlem48  43370  fourierdlem49  43371  fourierdlem62  43384  fourierdlem71  43393  fouriersw  43447  qndenserrnbllem  43510  qndenserrn  43515  salgencntex  43557  fsumlesge0  43590  sge0tsms  43593  sge0cl  43594  sge0f1o  43595  sge0sup  43604  sge0resplit  43619  sge0iunmptlemre  43628  sge0fodjrnlem  43629  sge0rpcpnf  43634  sge0xaddlem1  43646  ovolval4lem2  43863  sssmf  43946  smflimlem3  43980  smfsuplem1  44016  fcores  44233  prproropf1olem2  44629  zrinitorngc  45231  zrtermorngc  45232  zrzeroorngc  45233  irinitoringc  45300  zrtermoringc  45301  zrninitoringc  45302  nzerooringczr  45303  thincciso  46003