Theorem elind 4092

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

Syntax hints:   → wi 4   ∈ wcel 2081   ∩ cin 3858

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1777  ax-4 1791  ax-5 1888  ax-6 1947  ax-7 1992  ax-8 2083  ax-9 2091  ax-10 2112  ax-11 2126  ax-12 2141  ax-ext 2769

This theorem depends on definitions:  df-bi 208  df-an 397  df-or 843  df-tru 1525  df-ex 1762  df-nf 1766  df-sb 2043  df-clab 2776  df-cleq 2788  df-clel 2863  df-nfc 2935  df-v 3439  df-in 3866

This theorem is referenced by:  fvelimad  6600  fnfvimad  6861  tfrlem5  7868  uniinqs  8227  unifpw  8673  f1opwfi  8674  fissuni  8675  fipreima  8676  elfir  8725  inelfi  8728  cantnfcl  8976  tskwe  9225  infpwfidom  9300  infpwfien  9334  ackbij2lem1  9487  ackbij1lem3  9490  ackbij1lem4  9491  ackbij1lem6  9493  ackbij1lem11  9498  fin23lem24  9590  isfin1-3  9654  fpwwe2lem12  9909  fpwwe  9914  canthnumlem  9916  fz1isolem  13667  isprm7  15881  setsstruct2  16350  strfv2d  16358  submre  16705  submrc  16728  isacs2  16753  coffth  17035  catcoppccl  17197  catcfuccl  17198  catcxpccl  17286  isdrs2  17378  fpwipodrs  17603  sylow2a  18474  lsmmod  18528  lsmdisj  18534  lsmdisj2  18535  subgdisj1  18544  frgpnabllem1  18716  dmdprdd  18838  dprdfeq0  18861  dprdres  18867  dprddisj2  18878  dprd2da  18881  dmdprdsplit2lem  18884  ablfacrp  18905  pgpfac1lem3a  18915  pgpfac1lem3  18916  pgpfaclem1  18920  cntzsdrg  19271  aspval  19790  mplind  19969  zringlpirlem1  20313  zringlpirlem3  20315  pmatcoe1fsupp  20993  baspartn  21246  bastg  21258  clsval2  21342  isopn3  21358  restbas  21450  lmss  21590  cmpcovf  21683  discmp  21690  cmpsublem  21691  cmpsub  21692  isconn2  21706  connclo  21707  llynlly  21769  restnlly  21774  restlly  21775  islly2  21776  llyrest  21777  nllyrest  21778  llyidm  21780  nllyidm  21781  hausllycmp  21786  cldllycmp  21787  lly1stc  21788  dislly  21789  llycmpkgen2  21842  1stckgenlem  21845  txlly  21928  txnlly  21929  txtube  21932  txcmplem1  21933  txcmplem2  21934  xkococnlem  21951  basqtop  22003  tgqtop  22004  infil  22155  fmfnfmlem4  22249  hauspwpwf1  22279  tgpconncompss  22405  ustfilxp  22504  metrest  22817  tgioo  23087  zdis  23107  icccmplem1  23113  icccmplem2  23114  reconnlem2  23118  xrge0tsms  23125  cnheibor  23242  cnllycmp  23243  ncvs1  23444  cphsqrtcl  23471  cmetcaulem  23574  ovollb2lem  23772  ovolctb  23774  ovolshftlem1  23793  ovolscalem1  23797  ovolicc1  23800  ioombl1lem1  23842  ioorf  23857  ioorcl  23861  dyadf  23875  vitalilem2  23893  vitali  23897  i1faddlem  23977  i1fmullem  23978  dvres2lem  24191  dvaddbr  24218  dvmulbr  24219  lhop1lem  24293  lhop  24296  dvcnvrelem2  24298  ig1peu  24448  tayl0  24633  rlimcnp2  25226  xrlimcnp  25228  ppisval  25363  ppisval2  25364  ppinprm  25411  chtnprm  25413  2sqlem7  25682  chebbnd1lem1  25727  footexALT  26186  footexlem2  26188  foot  26190  footne  26191  perprag  26194  colperpexlem3  26200  mideulem2  26202  lnopp2hpgb  26231  colopp  26237  lmieu  26252  lmimid  26262  hypcgrlem1  26267  hypcgrlem2  26268  trgcopyeulem  26273  f1otrg  26340  eengtrkg  26455  wlkresOLD  27137  shuni  28768  5oalem1  29122  5oalem2  29123  5oalem4  29125  5oalem5  29126  3oalem2  29131  pjclem4  29667  pj3si  29675  xrge0tsmsd  30503  lindsunlem  30624  lbsdiflsp0  30626  dimkerim  30627  cmpcref  30731  cmppcmp  30739  dispcmp  30740  prsdm  30774  prsrn  30775  pnfneige0  30811  qqhucn  30850  rrhqima  30872  gsumesum  30935  esumcst  30939  esum2d  30969  sigainb  31012  inelpisys  31030  dynkin  31043  eulerpartlemgh  31253  eulerpartlemgs2  31255  eulerpartlemn  31256  sseqmw  31266  sseqf  31267  sseqp1  31270  fibp1  31276  bnj1379  31719  bnj1177  31892  cnllysconn  32101  rellysconn  32107  cvmsss2  32130  cvmcov2  32131  cvmopnlem  32134  mclsind  32426  frrlem15  32752  poimirlem30  34472  blbnd  34616  ssbnd  34617  heiborlem1  34640  heiborlem8  34647  heibor  34650  mndomgmid  34700  pmodlem1  36532  pclfinN  36586  mapdunirnN  38336  hdmaprnlem9N  38543  elrfi  38795  elrfirn  38796  fnwe2lem2  39155  dfac11  39166  kelac1  39167  kelac2lem  39168  dfac21  39170  islssfgi  39176  filnm  39194  lpirlnr  39221  hbtlem6  39233  hbt  39234  iocinico  39322  restuni3  40943  disjinfi  41013  fvelima2  41092  iooabslt  41335  iocopn  41357  icoopn  41362  uzinico  41397  limciccioolb  41463  limcicciooub  41479  islpcn  41481  limcresioolb  41485  limcleqr  41486  limsuppnfdlem  41543  limsupresxr  41608  liminfresxr  41609  liminfvalxr  41625  liminflelimsupuz  41627  cnrefiisplem  41671  ioccncflimc  41729  icccncfext  41731  icocncflimc  41733  cncfiooicclem1  41737  itgiccshift  41826  itgperiod  41827  itgsbtaddcnst  41828  stoweidlem57  41904  fourierdlem20  41974  fourierdlem32  41986  fourierdlem33  41987  fourierdlem48  42001  fourierdlem49  42002  fourierdlem62  42015  fourierdlem71  42024  fouriersw  42078  qndenserrnbllem  42141  qndenserrn  42146  salgencntex  42188  fsumlesge0  42221  sge0tsms  42224  sge0cl  42225  sge0f1o  42226  sge0sup  42235  sge0resplit  42250  sge0iunmptlemre  42259  sge0fodjrnlem  42260  sge0rpcpnf  42265  sge0xaddlem1  42277  ovolval4lem2  42494  sssmf  42577  smflimlem3  42611  smfsuplem1  42647  prproropf1olem2  43168  zrinitorngc  43769  zrtermorngc  43770  zrzeroorngc  43771  irinitoringc  43838  zrtermoringc  43839  zrninitoringc  43840  nzerooringczr  43841