Theorem elind 4153

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

Syntax hints:   → wi 4   ∈ wcel 2143   ∩ cin 3904

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1573  df-ex 1810  df-sb 2097  df-clab 2742  df-cleq 2755  df-clel 2838  df-v 3457  df-in 3912

This theorem is referenced by:  fvelima2  6933  fvelimad  6948  fnfvimad  7232  tfrlem5  8362  uniinqs  8791  unifpw  9308  f1opwfi  9309  fissuni  9310  fipreima  9311  elfir  9371  inelfi  9374  cantnfcl  9632  frrlem15  9725  tskwe  9932  infpwfidom  10008  infpwfien  10042  ackbij2lem1  10197  ackbij1lem3  10200  ackbij1lem4  10201  ackbij1lem6  10203  ackbij1lem11  10208  fin23lem24  10301  isfin1-3  10365  fpwwe2lem11  10621  fpwwe  10626  canthnumlem  10628  fz1isolem  14494  isprm7  16762  setsstruct2  17229  strfv2d  17256  submre  17652  submrc  17679  isacs2  17704  coffth  17990  catcoppccl  18169  catcfuccl  18170  catcxpccl  18258  isdrs2  18357  fpwipodrs  18591  insubm  18872  sylow2a  19684  lsmmod  19740  lsmdisj  19746  lsmdisj2  19747  subgdisj1  19756  frgpnabllem1  19938  dmdprdd  20066  dprdfeq0  20089  dprdres  20095  dprddisj2  20106  dprd2da  20109  dmdprdsplit2lem  20112  ablfacrp  20133  pgpfac1lem3a  20143  pgpfac1lem3  20144  pgpfaclem1  20148  zrinitorngc  20741  zrtermorngc  20742  zrzeroorngc  20743  zrtermoringc  20774  zrninitoringc  20775  cntzsdrg  20905  2idl0  21399  2idl1  21400  ssdifidlprm  21486  zringlpirlem1  21612  zringlpirlem3  21614  irinitoringc  21629  nzerooringczr  21630  aspval  22022  mplind  22221  pmatcoe1fsupp  22858  baspartn  23111  bastg  23123  clsval2  23207  isopn3  23223  restbas  23315  lmss  23455  cmpcovf  23548  discmp  23555  cmpsublem  23556  cmpsub  23557  isconn2  23571  connclo  23572  llynlly  23634  restnlly  23639  restlly  23640  islly2  23641  llyrest  23642  nllyrest  23643  llyidm  23645  nllyidm  23646  hausllycmp  23651  cldllycmp  23652  lly1stc  23653  dislly  23654  llycmpkgen2  23707  1stckgenlem  23710  txlly  23793  txnlly  23794  txtube  23797  txcmplem1  23798  txcmplem2  23799  xkococnlem  23816  basqtop  23868  tgqtop  23869  infil  24020  fmfnfmlem4  24114  hauspwpwf1  24144  tgpconncompss  24271  ustfilxp  24370  metrest  24681  tgioo  24953  zdis  24974  icccmplem1  24980  icccmplem2  24981  reconnlem2  24985  xrge0tsms  24992  cnheibor  25114  cnllycmp  25115  ncvs1  25316  cphsqrtcl  25343  cmetcaulem  25447  ovollb2lem  25647  ovolctb  25649  ovolshftlem1  25668  ovolscalem1  25672  ovolicc1  25675  ioombl1lem1  25717  ioorf  25732  ioorcl  25736  dyadf  25750  vitalilem2  25768  vitali  25772  i1faddlem  25852  i1fmullem  25853  dvres2lem  26069  dvaddbr  26097  dvmulbr  26098  lhop1lem  26172  lhop  26175  dvcnvrelem2  26177  ig1peu  26332  tayl0  26525  rlimcnp2  27131  xrlimcnp  27133  ppisval  27268  ppisval2  27269  ppinprm  27316  chtnprm  27318  2sqlem7  27588  chebbnd1lem1  27633  tglnpt4  28928  footexALT  28998  footexlem2  29000  foot  29002  footne  29003  perprag  29007  colperpexlem3  29013  mideulem2  29015  lnopp2hpgb  29045  colopp  29051  lnincplng  29066  plngrotlem1  29069  plngrotlem2  29070  lnssplng  29074  lmieu  29093  lmimid  29103  hypcgrlem1  29109  hypcgrlem2  29110  trgcopyeulem  29116  dfprlng2  29197  prlngmolem1  29202  prlngmolem2  29203  prlngmo2  29206  prlngpln4  29208  prlngmid2  29211  prlngsymquadlem  29213  quadcgrprlng  29216  f1otrg  29220  eengtrkg  29336  shuni  31652  5oalem1  32006  5oalem2  32007  5oalem4  32009  5oalem5  32010  3oalem2  32015  pjclem4  32551  pj3si  32559  ccatf1  33269  xrge0tsmsd  33393  wrdpmtrlast  33413  idlinsubrg  33739  qsdrngilem  33776  qsdrngi  33777  pidufd  33833  exsslsb  33987  lindsunlem  34014  lbsdiflsp0  34016  dimkerim  34017  irngss  34077  cmpcref  34240  cmppcmp  34248  dispcmp  34249  zarcmplem  34271  prsdm  34304  prsrn  34305  pnfneige0  34341  qqhucn  34382  rrhqima  34404  gsumesum  34449  esumcst  34453  esum2d  34483  sigainb  34526  inelpisys  34544  dynkin  34557  eulerpartlemgh  34768  eulerpartlemgs2  34770  eulerpartlemn  34771  sseqmw  34781  sseqf  34782  sseqp1  34785  fibp1  34791  bnj1379  35218  bnj1177  35394  cnllysconn  35737  rellysconn  35743  cvmsss2  35766  cvmcov2  35767  cvmopnlem  35770  mclsind  36062  weiunfr  36978  poimirlem30  38301  blbnd  38438  ssbnd  38439  heiborlem1  38462  heiborlem8  38469  heibor  38472  mndomgmid  38522  pmodlem1  40620  pclfinN  40674  mapdunirnN  42424  hdmaprnlem9N  42631  mhpind  43326  elrfi  43425  elrfirn  43426  fnwe2lem2  43778  dfac11  43789  kelac1  43790  kelac2lem  43791  dfac21  43793  islssfgi  43799  filnm  43817  lpirlnr  43844  hbtlem6  43856  hbt  43857  iocinico  43939  restuni3  45836  disjinfi  45910  iooabslt  46215  iocopn  46236  icoopn  46241  uzinico  46275  limciccioolb  46337  limcicciooub  46351  islpcn  46353  limcresioolb  46357  limcleqr  46358  limsuppnfdlem  46415  limsupresxr  46480  liminfresxr  46481  liminfvalxr  46497  liminflelimsupuz  46499  cnrefiisplem  46543  ioccncflimc  46599  icccncfext  46601  icocncflimc  46603  cncfiooicclem1  46607  itgiccshift  46694  itgperiod  46695  itgsbtaddcnst  46696  stoweidlem57  46771  fourierdlem20  46841  fourierdlem32  46853  fourierdlem33  46854  fourierdlem48  46868  fourierdlem49  46869  fourierdlem62  46882  fourierdlem71  46891  fouriersw  46945  qndenserrnbllem  47008  qndenserrn  47013  salgencntex  47057  fsumlesge0  47091  sge0tsms  47094  sge0cl  47095  sge0f1o  47096  sge0sup  47105  sge0resplit  47120  sge0iunmptlemre  47129  sge0fodjrnlem  47130  sge0rpcpnf  47135  sge0xaddlem1  47147  ovolval4lem2  47364  sssmf  47452  smflimlem3  47487  smfsuplem1  47525  fcores  47804  prproropf1olem2  48253  iinfconstbaslem  49843  ffthoppf  49943  uobeqw  49997  uobeq  49998  swapfiso  50063  swapciso  50064  fucoppcffth  50189  thincciso  50231  thinccisod  50232  termcterm  50291  termcterm2  50292  termcterm3  50293  termcciso  50294  termc2  50296  diagciso  50317  diagcic  50318  uobeqterm  50324