Theorem elind 4149

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

Syntax hints:   → wi 4   ∈ wcel 2113   ∩ cin 3897

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2712  df-cleq 2725  df-clel 2808  df-v 3439  df-in 3905

This theorem is referenced by:  fvelima2  6883  fvelimad  6898  fnfvimad  7177  tfrlem5  8308  uniinqs  8730  unifpw  9250  f1opwfi  9251  fissuni  9252  fipreima  9253  elfir  9310  inelfi  9313  cantnfcl  9568  frrlem15  9661  tskwe  9854  infpwfidom  9930  infpwfien  9964  ackbij2lem1  10120  ackbij1lem3  10123  ackbij1lem4  10124  ackbij1lem6  10126  ackbij1lem11  10131  fin23lem24  10224  isfin1-3  10288  fpwwe2lem11  10543  fpwwe  10548  canthnumlem  10550  fz1isolem  14375  isprm7  16626  setsstruct2  17092  strfv2d  17119  submre  17515  submrc  17542  isacs2  17567  coffth  17853  catcoppccl  18032  catcfuccl  18033  catcxpccl  18121  isdrs2  18220  fpwipodrs  18454  insubm  18734  sylow2a  19539  lsmmod  19595  lsmdisj  19601  lsmdisj2  19602  subgdisj1  19611  frgpnabllem1  19793  dmdprdd  19921  dprdfeq0  19944  dprdres  19950  dprddisj2  19961  dprd2da  19964  dmdprdsplit2lem  19967  ablfacrp  19988  pgpfac1lem3a  19998  pgpfac1lem3  19999  pgpfaclem1  20003  zrinitorngc  20566  zrtermorngc  20567  zrzeroorngc  20568  zrtermoringc  20599  zrninitoringc  20600  cntzsdrg  20726  2idl0  21206  2idl1  21207  zringlpirlem1  21408  zringlpirlem3  21410  irinitoringc  21425  nzerooringczr  21426  aspval  21819  mplind  22016  pmatcoe1fsupp  22636  baspartn  22889  bastg  22901  clsval2  22985  isopn3  23001  restbas  23093  lmss  23233  cmpcovf  23326  discmp  23333  cmpsublem  23334  cmpsub  23335  isconn2  23349  connclo  23350  llynlly  23412  restnlly  23417  restlly  23418  islly2  23419  llyrest  23420  nllyrest  23421  llyidm  23423  nllyidm  23424  hausllycmp  23429  cldllycmp  23430  lly1stc  23431  dislly  23432  llycmpkgen2  23485  1stckgenlem  23488  txlly  23571  txnlly  23572  txtube  23575  txcmplem1  23576  txcmplem2  23577  xkococnlem  23594  basqtop  23646  tgqtop  23647  infil  23798  fmfnfmlem4  23892  hauspwpwf1  23922  tgpconncompss  24049  ustfilxp  24148  metrest  24459  tgioo  24731  zdis  24752  icccmplem1  24758  icccmplem2  24759  reconnlem2  24763  xrge0tsms  24770  cnheibor  24901  cnllycmp  24902  ncvs1  25104  cphsqrtcl  25131  cmetcaulem  25235  ovollb2lem  25436  ovolctb  25438  ovolshftlem1  25457  ovolscalem1  25461  ovolicc1  25464  ioombl1lem1  25506  ioorf  25521  ioorcl  25525  dyadf  25539  vitalilem2  25557  vitali  25561  i1faddlem  25641  i1fmullem  25642  dvres2lem  25858  dvaddbr  25887  dvmulbr  25888  dvmulbrOLD  25889  lhop1lem  25965  lhop  25968  dvcnvrelem2  25970  ig1peu  26127  tayl0  26316  rlimcnp2  26923  xrlimcnp  26925  ppisval  27061  ppisval2  27062  ppinprm  27109  chtnprm  27111  2sqlem7  27382  chebbnd1lem1  27427  footexALT  28716  footexlem2  28718  foot  28720  footne  28721  perprag  28724  colperpexlem3  28730  mideulem2  28732  lnopp2hpgb  28761  colopp  28767  lmieu  28782  lmimid  28792  hypcgrlem1  28797  hypcgrlem2  28798  trgcopyeulem  28803  f1otrg  28869  eengtrkg  28985  shuni  31301  5oalem1  31655  5oalem2  31656  5oalem4  31658  5oalem5  31659  3oalem2  31664  pjclem4  32200  pj3si  32208  ccatf1  32959  xrge0tsmsd  33083  wrdpmtrlast  33103  idlinsubrg  33440  ssdifidlprm  33467  qsdrngilem  33503  qsdrngi  33504  pidufd  33552  exsslsb  33681  lindsunlem  33709  lbsdiflsp0  33711  dimkerim  33712  irngss  33772  cmpcref  33935  cmppcmp  33943  dispcmp  33944  zarcmplem  33966  prsdm  33999  prsrn  34000  pnfneige0  34036  qqhucn  34077  rrhqima  34099  gsumesum  34144  esumcst  34148  esum2d  34178  sigainb  34221  inelpisys  34239  dynkin  34252  eulerpartlemgh  34463  eulerpartlemgs2  34465  eulerpartlemn  34466  sseqmw  34476  sseqf  34477  sseqp1  34480  fibp1  34486  bnj1379  34914  bnj1177  35090  cnllysconn  35361  rellysconn  35367  cvmsss2  35390  cvmcov2  35391  cvmopnlem  35394  mclsind  35686  weiunfr  36583  poimirlem30  37763  blbnd  37900  ssbnd  37901  heiborlem1  37924  heiborlem8  37931  heibor  37934  mndomgmid  37984  pmodlem1  40018  pclfinN  40072  mapdunirnN  41822  hdmaprnlem9N  42029  mhpind  42752  elrfi  42851  elrfirn  42852  fnwe2lem2  43208  dfac11  43219  kelac1  43220  kelac2lem  43221  dfac21  43223  islssfgi  43229  filnm  43247  lpirlnr  43274  hbtlem6  43286  hbt  43287  iocinico  43369  restuni3  45278  disjinfi  45352  iooabslt  45661  iocopn  45682  icoopn  45687  uzinico  45721  limciccioolb  45783  limcicciooub  45797  islpcn  45799  limcresioolb  45803  limcleqr  45804  limsuppnfdlem  45861  limsupresxr  45926  liminfresxr  45927  liminfvalxr  45943  liminflelimsupuz  45945  cnrefiisplem  45989  ioccncflimc  46045  icccncfext  46047  icocncflimc  46049  cncfiooicclem1  46053  itgiccshift  46140  itgperiod  46141  itgsbtaddcnst  46142  stoweidlem57  46217  fourierdlem20  46287  fourierdlem32  46299  fourierdlem33  46300  fourierdlem48  46314  fourierdlem49  46315  fourierdlem62  46328  fourierdlem71  46337  fouriersw  46391  qndenserrnbllem  46454  qndenserrn  46459  salgencntex  46503  fsumlesge0  46537  sge0tsms  46540  sge0cl  46541  sge0f1o  46542  sge0sup  46551  sge0resplit  46566  sge0iunmptlemre  46575  sge0fodjrnlem  46576  sge0rpcpnf  46581  sge0xaddlem1  46593  ovolval4lem2  46810  sssmf  46898  smflimlem3  46933  smfsuplem1  46971  fcores  47229  prproropf1olem2  47666  iinfconstbaslem  49226  ffthoppf  49326  uobeqw  49380  uobeq  49381  swapfiso  49446  swapciso  49447  fucoppcffth  49572  thincciso  49614  thinccisod  49615  termcterm  49674  termcterm2  49675  termcterm3  49676  termcciso  49677  termc2  49679  diagciso  49700  diagcic  49701  uobeqterm  49707