Theorem elind 4193

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

Syntax hints:   → wi 4   ∈ wcel 2106   ∩ cin 3946

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-ext 2703

This theorem depends on definitions:  df-bi 206  df-an 397  df-tru 1544  df-ex 1782  df-sb 2068  df-clab 2710  df-cleq 2724  df-clel 2810  df-v 3476  df-in 3954

This theorem is referenced by:  fvelimad  6956  fnfvimad  7232  tfrlem5  8376  uniinqs  8787  unifpw  9351  f1opwfi  9352  fissuni  9353  fipreima  9354  elfir  9406  inelfi  9409  cantnfcl  9658  frrlem15  9748  tskwe  9941  infpwfidom  10019  infpwfien  10053  ackbij2lem1  10210  ackbij1lem3  10213  ackbij1lem4  10214  ackbij1lem6  10216  ackbij1lem11  10221  fin23lem24  10313  isfin1-3  10377  fpwwe2lem11  10632  fpwwe  10637  canthnumlem  10639  fz1isolem  14418  isprm7  16641  setsstruct2  17103  strfv2d  17131  submre  17545  submrc  17568  isacs2  17593  coffth  17883  catcoppccl  18063  catcoppcclOLD  18064  catcfuccl  18065  catcfucclOLD  18066  catcxpccl  18155  catcxpcclOLD  18156  isdrs2  18255  fpwipodrs  18489  insubm  18695  sylow2a  19481  lsmmod  19537  lsmdisj  19543  lsmdisj2  19544  subgdisj1  19553  frgpnabllem1  19735  dmdprdd  19863  dprdfeq0  19886  dprdres  19892  dprddisj2  19903  dprd2da  19906  dmdprdsplit2lem  19909  ablfacrp  19930  pgpfac1lem3a  19940  pgpfac1lem3  19941  pgpfaclem1  19945  cntzsdrg  20410  2idl0  20855  2idl1  20856  zringlpirlem1  21023  zringlpirlem3  21025  aspval  21418  mplind  21622  pmatcoe1fsupp  22194  baspartn  22448  bastg  22460  clsval2  22545  isopn3  22561  restbas  22653  lmss  22793  cmpcovf  22886  discmp  22893  cmpsublem  22894  cmpsub  22895  isconn2  22909  connclo  22910  llynlly  22972  restnlly  22977  restlly  22978  islly2  22979  llyrest  22980  nllyrest  22981  llyidm  22983  nllyidm  22984  hausllycmp  22989  cldllycmp  22990  lly1stc  22991  dislly  22992  llycmpkgen2  23045  1stckgenlem  23048  txlly  23131  txnlly  23132  txtube  23135  txcmplem1  23136  txcmplem2  23137  xkococnlem  23154  basqtop  23206  tgqtop  23207  infil  23358  fmfnfmlem4  23452  hauspwpwf1  23482  tgpconncompss  23609  ustfilxp  23708  metrest  24024  tgioo  24303  zdis  24323  icccmplem1  24329  icccmplem2  24330  reconnlem2  24334  xrge0tsms  24341  cnheibor  24462  cnllycmp  24463  ncvs1  24665  cphsqrtcl  24692  cmetcaulem  24796  ovollb2lem  24996  ovolctb  24998  ovolshftlem1  25017  ovolscalem1  25021  ovolicc1  25024  ioombl1lem1  25066  ioorf  25081  ioorcl  25085  dyadf  25099  vitalilem2  25117  vitali  25121  i1faddlem  25201  i1fmullem  25202  dvres2lem  25418  dvaddbr  25446  dvmulbr  25447  lhop1lem  25521  lhop  25524  dvcnvrelem2  25526  ig1peu  25680  tayl0  25865  rlimcnp2  26460  xrlimcnp  26462  ppisval  26597  ppisval2  26598  ppinprm  26645  chtnprm  26647  2sqlem7  26916  chebbnd1lem1  26961  footexALT  27958  footexlem2  27960  foot  27962  footne  27963  perprag  27966  colperpexlem3  27972  mideulem2  27974  lnopp2hpgb  28003  colopp  28009  lmieu  28024  lmimid  28034  hypcgrlem1  28039  hypcgrlem2  28040  trgcopyeulem  28045  f1otrg  28111  eengtrkg  28233  shuni  30540  5oalem1  30894  5oalem2  30895  5oalem4  30897  5oalem5  30898  3oalem2  30903  pjclem4  31439  pj3si  31447  ccatf1  32102  xrge0tsmsd  32196  idlinsubrg  32537  qsdrngilem  32596  qsdrngi  32597  lindsunlem  32697  lbsdiflsp0  32699  dimkerim  32700  irngss  32739  cmpcref  32818  cmppcmp  32826  dispcmp  32827  zarcmplem  32849  prsdm  32882  prsrn  32883  pnfneige0  32919  qqhucn  32960  rrhqima  32982  gsumesum  33045  esumcst  33049  esum2d  33079  sigainb  33122  inelpisys  33140  dynkin  33153  eulerpartlemgh  33365  eulerpartlemgs2  33367  eulerpartlemn  33368  sseqmw  33378  sseqf  33379  sseqp1  33382  fibp1  33388  bnj1379  33829  bnj1177  34005  cnllysconn  34224  rellysconn  34230  cvmsss2  34253  cvmcov2  34254  cvmopnlem  34257  mclsind  34549  gg-dvmulbr  35163  poimirlem30  36506  blbnd  36643  ssbnd  36644  heiborlem1  36667  heiborlem8  36674  heibor  36677  mndomgmid  36727  pmodlem1  38705  pclfinN  38759  mapdunirnN  40509  hdmaprnlem9N  40716  mhpind  41163  elrfi  41417  elrfirn  41418  fnwe2lem2  41778  dfac11  41789  kelac1  41790  kelac2lem  41791  dfac21  41793  islssfgi  41799  filnm  41817  lpirlnr  41844  hbtlem6  41856  hbt  41857  iocinico  41946  restuni3  43792  disjinfi  43876  fvelima2  43950  iooabslt  44198  iocopn  44219  icoopn  44224  uzinico  44259  limciccioolb  44323  limcicciooub  44339  islpcn  44341  limcresioolb  44345  limcleqr  44346  limsuppnfdlem  44403  limsupresxr  44468  liminfresxr  44469  liminfvalxr  44485  liminflelimsupuz  44487  cnrefiisplem  44531  ioccncflimc  44587  icccncfext  44589  icocncflimc  44591  cncfiooicclem1  44595  itgiccshift  44682  itgperiod  44683  itgsbtaddcnst  44684  stoweidlem57  44759  fourierdlem20  44829  fourierdlem32  44841  fourierdlem33  44842  fourierdlem48  44856  fourierdlem49  44857  fourierdlem62  44870  fourierdlem71  44879  fouriersw  44933  qndenserrnbllem  44996  qndenserrn  45001  salgencntex  45045  fsumlesge0  45079  sge0tsms  45082  sge0cl  45083  sge0f1o  45084  sge0sup  45093  sge0resplit  45108  sge0iunmptlemre  45117  sge0fodjrnlem  45118  sge0rpcpnf  45123  sge0xaddlem1  45135  ovolval4lem2  45352  sssmf  45440  smflimlem3  45475  smfsuplem1  45513  fcores  45763  prproropf1olem2  46158  zrinitorngc  46851  zrtermorngc  46852  zrzeroorngc  46853  irinitoringc  46920  zrtermoringc  46921  zrninitoringc  46922  nzerooringczr  46923  thincciso  47622