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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1802  ax-4 1816  ax-5 1917  ax-6 1974  ax-7 2015  ax-8 2121  ax-9 2129  ax-ext 2711

This theorem depends on definitions:  df-bi 208  df-an 397  df-tru 1550  df-ex 1787  df-sb 2074  df-clab 2718  df-cleq 2731  df-clel 2814  df-v 3433  df-in 3890

This theorem is referenced by:  fvelima2  6879  fvelimad  6894  fnfvimad  7178  tfrlem5  8309  uniinqs  8734  unifpw  9255  f1opwfi  9256  fissuni  9257  fipreima  9258  elfir  9318  inelfi  9321  cantnfcl  9579  frrlem15  9672  tskwe  9865  infpwfidom  9941  infpwfien  9975  ackbij2lem1  10131  ackbij1lem3  10134  ackbij1lem4  10135  ackbij1lem6  10137  ackbij1lem11  10142  fin23lem24  10235  isfin1-3  10299  fpwwe2lem11  10555  fpwwe  10560  canthnumlem  10562  fz1isolem  14414  isprm7  16669  setsstruct2  17135  strfv2d  17162  submre  17558  submrc  17585  isacs2  17610  coffth  17896  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  isdrs2  18263  fpwipodrs  18497  insubm  18777  sylow2a  19585  lsmmod  19641  lsmdisj  19647  lsmdisj2  19648  subgdisj1  19657  frgpnabllem1  19839  dmdprdd  19967  dprdfeq0  19990  dprdres  19996  dprddisj2  20007  dprd2da  20010  dmdprdsplit2lem  20013  ablfacrp  20034  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfaclem1  20049  zrinitorngc  20614  zrtermorngc  20615  zrzeroorngc  20616  zrtermoringc  20647  zrninitoringc  20648  cntzsdrg  20774  2idl0  21253  2idl1  21254  zringlpirlem1  21437  zringlpirlem3  21439  irinitoringc  21454  nzerooringczr  21455  aspval  21847  mplind  22046  pmatcoe1fsupp  22684  baspartn  22937  bastg  22949  clsval2  23033  isopn3  23049  restbas  23141  lmss  23281  cmpcovf  23374  discmp  23381  cmpsublem  23382  cmpsub  23383  isconn2  23397  connclo  23398  llynlly  23460  restnlly  23465  restlly  23466  islly2  23467  llyrest  23468  nllyrest  23469  llyidm  23471  nllyidm  23472  hausllycmp  23477  cldllycmp  23478  lly1stc  23479  dislly  23480  llycmpkgen2  23533  1stckgenlem  23536  txlly  23619  txnlly  23620  txtube  23623  txcmplem1  23624  txcmplem2  23625  xkococnlem  23642  basqtop  23694  tgqtop  23695  infil  23846  fmfnfmlem4  23940  hauspwpwf1  23970  tgpconncompss  24097  ustfilxp  24196  metrest  24507  tgioo  24779  zdis  24800  icccmplem1  24806  icccmplem2  24807  reconnlem2  24811  xrge0tsms  24818  cnheibor  24940  cnllycmp  24941  ncvs1  25142  cphsqrtcl  25169  cmetcaulem  25273  ovollb2lem  25473  ovolctb  25475  ovolshftlem1  25494  ovolscalem1  25498  ovolicc1  25501  ioombl1lem1  25543  ioorf  25558  ioorcl  25562  dyadf  25576  vitalilem2  25594  vitali  25598  i1faddlem  25678  i1fmullem  25679  dvres2lem  25895  dvaddbr  25923  dvmulbr  25924  lhop1lem  25998  lhop  26001  dvcnvrelem2  26003  ig1peu  26158  tayl0  26345  rlimcnp2  26948  xrlimcnp  26950  ppisval  27085  ppisval2  27086  ppinprm  27133  chtnprm  27135  2sqlem7  27405  chebbnd1lem1  27450  footexALT  28804  footexlem2  28806  foot  28808  footne  28809  perprag  28812  colperpexlem3  28818  mideulem2  28820  lnopp2hpgb  28849  colopp  28855  lmieu  28870  lmimid  28880  hypcgrlem1  28885  hypcgrlem2  28886  trgcopyeulem  28891  f1otrg  28957  eengtrkg  29073  shuni  31389  5oalem1  31743  5oalem2  31744  5oalem4  31746  5oalem5  31747  3oalem2  31752  pjclem4  32288  pj3si  32296  ccatf1  33028  xrge0tsmsd  33154  wrdpmtrlast  33174  idlinsubrg  33514  ssdifidlprm  33541  qsdrngilem  33577  qsdrngi  33578  pidufd  33626  exsslsb  33781  lindsunlem  33808  lbsdiflsp0  33810  dimkerim  33811  irngss  33871  cmpcref  34034  cmppcmp  34042  dispcmp  34043  zarcmplem  34065  prsdm  34098  prsrn  34099  pnfneige0  34135  qqhucn  34176  rrhqima  34198  gsumesum  34243  esumcst  34247  esum2d  34277  sigainb  34320  inelpisys  34338  dynkin  34351  eulerpartlemgh  34562  eulerpartlemgs2  34564  eulerpartlemn  34565  sseqmw  34575  sseqf  34576  sseqp1  34579  fibp1  34585  bnj1379  35012  bnj1177  35188  cnllysconn  35473  rellysconn  35479  cvmsss2  35502  cvmcov2  35503  cvmopnlem  35506  mclsind  35798  weiunfr  36695  poimirlem30  38017  blbnd  38154  ssbnd  38155  heiborlem1  38178  heiborlem8  38185  heibor  38188  mndomgmid  38238  pmodlem1  40338  pclfinN  40392  mapdunirnN  42142  hdmaprnlem9N  42349  mhpind  43044  elrfi  43143  elrfirn  43144  fnwe2lem2  43496  dfac11  43507  kelac1  43508  kelac2lem  43509  dfac21  43511  islssfgi  43517  filnm  43535  lpirlnr  43562  hbtlem6  43574  hbt  43575  iocinico  43657  restuni3  45565  disjinfi  45639  iooabslt  45944  iocopn  45965  icoopn  45970  uzinico  46004  limciccioolb  46066  limcicciooub  46080  islpcn  46082  limcresioolb  46086  limcleqr  46087  limsuppnfdlem  46144  limsupresxr  46209  liminfresxr  46210  liminfvalxr  46226  liminflelimsupuz  46228  cnrefiisplem  46272  ioccncflimc  46328  icccncfext  46330  icocncflimc  46332  cncfiooicclem1  46336  itgiccshift  46423  itgperiod  46424  itgsbtaddcnst  46425  stoweidlem57  46500  fourierdlem20  46570  fourierdlem32  46582  fourierdlem33  46583  fourierdlem48  46597  fourierdlem49  46598  fourierdlem62  46611  fourierdlem71  46620  fouriersw  46674  qndenserrnbllem  46737  qndenserrn  46742  salgencntex  46786  fsumlesge0  46820  sge0tsms  46823  sge0cl  46824  sge0f1o  46825  sge0sup  46834  sge0resplit  46849  sge0iunmptlemre  46858  sge0fodjrnlem  46859  sge0rpcpnf  46864  sge0xaddlem1  46876  ovolval4lem2  47093  sssmf  47181  smflimlem3  47216  smfsuplem1  47254  fcores  47530  prproropf1olem2  47979  iinfconstbaslem  49555  ffthoppf  49655  uobeqw  49709  uobeq  49710  swapfiso  49775  swapciso  49776  fucoppcffth  49901  thincciso  49943  thinccisod  49944  termcterm  50003  termcterm2  50004  termcterm3  50005  termcciso  50006  termc2  50008  diagciso  50029  diagcic  50030  uobeqterm  50036