Theorem elind 4155

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

Syntax hints:   → wi 4   ∈ wcel 2145   ∩ cin 3906

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1818  ax-4 1832  ax-5 1933  ax-6 1990  ax-7 2031  ax-8 2147  ax-9 2155  ax-ext 2737

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1566  df-ex 1803  df-sb 2094  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3914

This theorem is referenced by:  fvelima2  6923  fvelimad  6938  fnfvimad  7222  tfrlem5  8354  uniinqs  8783  unifpw  9300  f1opwfi  9301  fissuni  9302  fipreima  9303  elfir  9363  inelfi  9366  cantnfcl  9624  frrlem15  9717  tskwe  9924  infpwfidom  10000  infpwfien  10034  ackbij2lem1  10189  ackbij1lem3  10192  ackbij1lem4  10193  ackbij1lem6  10195  ackbij1lem11  10200  fin23lem24  10294  isfin1-3  10358  fpwwe2lem11  10614  fpwwe  10619  canthnumlem  10621  fz1isolem  14486  isprm7  16755  setsstruct2  17222  strfv2d  17249  submre  17645  submrc  17672  isacs2  17697  coffth  17983  catcoppccl  18162  catcfuccl  18163  catcxpccl  18251  isdrs2  18350  fpwipodrs  18584  insubm  18865  sylow2a  19677  lsmmod  19733  lsmdisj  19739  lsmdisj2  19740  subgdisj1  19749  frgpnabllem1  19931  dmdprdd  20059  dprdfeq0  20082  dprdres  20088  dprddisj2  20099  dprd2da  20102  dmdprdsplit2lem  20105  ablfacrp  20126  pgpfac1lem3a  20136  pgpfac1lem3  20137  pgpfaclem1  20141  zrinitorngc  20715  zrtermorngc  20716  zrzeroorngc  20717  zrtermoringc  20748  zrninitoringc  20749  cntzsdrg  20871  2idl0  21358  2idl1  21359  ssdifidlprm  21443  zringlpirlem1  21569  zringlpirlem3  21571  irinitoringc  21586  nzerooringczr  21587  aspval  21979  mplind  22178  pmatcoe1fsupp  22815  baspartn  23068  bastg  23080  clsval2  23164  isopn3  23180  restbas  23272  lmss  23412  cmpcovf  23505  discmp  23512  cmpsublem  23513  cmpsub  23514  isconn2  23528  connclo  23529  llynlly  23591  restnlly  23596  restlly  23597  islly2  23598  llyrest  23599  nllyrest  23600  llyidm  23602  nllyidm  23603  hausllycmp  23608  cldllycmp  23609  lly1stc  23610  dislly  23611  llycmpkgen2  23664  1stckgenlem  23667  txlly  23750  txnlly  23751  txtube  23754  txcmplem1  23755  txcmplem2  23756  xkococnlem  23773  basqtop  23825  tgqtop  23826  infil  23977  fmfnfmlem4  24071  hauspwpwf1  24101  tgpconncompss  24228  ustfilxp  24327  metrest  24638  tgioo  24910  zdis  24931  icccmplem1  24937  icccmplem2  24938  reconnlem2  24942  xrge0tsms  24949  cnheibor  25071  cnllycmp  25072  ncvs1  25273  cphsqrtcl  25300  cmetcaulem  25404  ovollb2lem  25604  ovolctb  25606  ovolshftlem1  25625  ovolscalem1  25629  ovolicc1  25632  ioombl1lem1  25674  ioorf  25689  ioorcl  25693  dyadf  25707  vitalilem2  25725  vitali  25729  i1faddlem  25809  i1fmullem  25810  dvres2lem  26026  dvaddbr  26054  dvmulbr  26055  lhop1lem  26129  lhop  26132  dvcnvrelem2  26134  ig1peu  26289  tayl0  26479  rlimcnp2  27085  xrlimcnp  27087  ppisval  27222  ppisval2  27223  ppinprm  27270  chtnprm  27272  2sqlem7  27542  chebbnd1lem1  27587  tglnpt4  28878  footexALT  28945  footexlem2  28947  foot  28949  footne  28950  perprag  28953  colperpexlem3  28959  mideulem2  28961  lnopp2hpgb  28990  colopp  28996  lnincplng  29010  plngrotlem1  29013  plngrotlem2  29014  lnssplng  29018  lmieu  29032  lmimid  29042  hypcgrlem1  29047  hypcgrlem2  29048  trgcopyeulem  29053  f1otrg  29125  eengtrkg  29241  shuni  31557  5oalem1  31911  5oalem2  31912  5oalem4  31914  5oalem5  31915  3oalem2  31920  pjclem4  32456  pj3si  32464  ccatf1  33177  xrge0tsmsd  33301  wrdpmtrlast  33321  idlinsubrg  33650  qsdrngilem  33688  qsdrngi  33689  pidufd  33745  exsslsb  33899  lindsunlem  33926  lbsdiflsp0  33928  dimkerim  33929  irngss  33989  cmpcref  34152  cmppcmp  34160  dispcmp  34161  zarcmplem  34183  prsdm  34216  prsrn  34217  pnfneige0  34253  qqhucn  34294  rrhqima  34316  gsumesum  34361  esumcst  34365  esum2d  34395  sigainb  34438  inelpisys  34456  dynkin  34469  eulerpartlemgh  34680  eulerpartlemgs2  34682  eulerpartlemn  34683  sseqmw  34693  sseqf  34694  sseqp1  34697  fibp1  34703  bnj1379  35130  bnj1177  35306  cnllysconn  35603  rellysconn  35609  cvmsss2  35632  cvmcov2  35633  cvmopnlem  35636  mclsind  35928  weiunfr  36835  poimirlem30  38156  blbnd  38293  ssbnd  38294  heiborlem1  38317  heiborlem8  38324  heibor  38327  mndomgmid  38377  pmodlem1  40477  pclfinN  40531  mapdunirnN  42281  hdmaprnlem9N  42488  mhpind  43183  elrfi  43282  elrfirn  43283  fnwe2lem2  43635  dfac11  43646  kelac1  43647  kelac2lem  43648  dfac21  43650  islssfgi  43656  filnm  43674  lpirlnr  43701  hbtlem6  43713  hbt  43714  iocinico  43796  restuni3  45695  disjinfi  45769  iooabslt  46074  iocopn  46095  icoopn  46100  uzinico  46134  limciccioolb  46196  limcicciooub  46210  islpcn  46212  limcresioolb  46216  limcleqr  46217  limsuppnfdlem  46274  limsupresxr  46339  liminfresxr  46340  liminfvalxr  46356  liminflelimsupuz  46358  cnrefiisplem  46402  ioccncflimc  46458  icccncfext  46460  icocncflimc  46462  cncfiooicclem1  46466  itgiccshift  46553  itgperiod  46554  itgsbtaddcnst  46555  stoweidlem57  46630  fourierdlem20  46700  fourierdlem32  46712  fourierdlem33  46713  fourierdlem48  46727  fourierdlem49  46728  fourierdlem62  46741  fourierdlem71  46750  fouriersw  46804  qndenserrnbllem  46867  qndenserrn  46872  salgencntex  46916  fsumlesge0  46950  sge0tsms  46953  sge0cl  46954  sge0f1o  46955  sge0sup  46964  sge0resplit  46979  sge0iunmptlemre  46988  sge0fodjrnlem  46989  sge0rpcpnf  46994  sge0xaddlem1  47006  ovolval4lem2  47223  sssmf  47311  smflimlem3  47346  smfsuplem1  47384  fcores  47660  prproropf1olem2  48109  iinfconstbaslem  49695  ffthoppf  49795  uobeqw  49849  uobeq  49850  swapfiso  49915  swapciso  49916  fucoppcffth  50041  thincciso  50083  thinccisod  50084  termcterm  50143  termcterm2  50144  termcterm3  50145  termcciso  50146  termc2  50148  diagciso  50169  diagcic  50170  uobeqterm  50176