Theorem elind 4152

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

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

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 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3442  df-in 3908

This theorem is referenced by:  fvelima2  6886  fvelimad  6901  fnfvimad  7180  tfrlem5  8311  uniinqs  8734  unifpw  9255  f1opwfi  9256  fissuni  9257  fipreima  9258  elfir  9318  inelfi  9321  cantnfcl  9576  frrlem15  9669  tskwe  9862  infpwfidom  9938  infpwfien  9972  ackbij2lem1  10128  ackbij1lem3  10131  ackbij1lem4  10132  ackbij1lem6  10134  ackbij1lem11  10139  fin23lem24  10232  isfin1-3  10296  fpwwe2lem11  10552  fpwwe  10557  canthnumlem  10559  fz1isolem  14384  isprm7  16635  setsstruct2  17101  strfv2d  17128  submre  17524  submrc  17551  isacs2  17576  coffth  17862  catcoppccl  18041  catcfuccl  18042  catcxpccl  18130  isdrs2  18229  fpwipodrs  18463  insubm  18743  sylow2a  19548  lsmmod  19604  lsmdisj  19610  lsmdisj2  19611  subgdisj1  19620  frgpnabllem1  19802  dmdprdd  19930  dprdfeq0  19953  dprdres  19959  dprddisj2  19970  dprd2da  19973  dmdprdsplit2lem  19976  ablfacrp  19997  pgpfac1lem3a  20007  pgpfac1lem3  20008  pgpfaclem1  20012  zrinitorngc  20575  zrtermorngc  20576  zrzeroorngc  20577  zrtermoringc  20608  zrninitoringc  20609  cntzsdrg  20735  2idl0  21215  2idl1  21216  zringlpirlem1  21417  zringlpirlem3  21419  irinitoringc  21434  nzerooringczr  21435  aspval  21828  mplind  22025  pmatcoe1fsupp  22645  baspartn  22898  bastg  22910  clsval2  22994  isopn3  23010  restbas  23102  lmss  23242  cmpcovf  23335  discmp  23342  cmpsublem  23343  cmpsub  23344  isconn2  23358  connclo  23359  llynlly  23421  restnlly  23426  restlly  23427  islly2  23428  llyrest  23429  nllyrest  23430  llyidm  23432  nllyidm  23433  hausllycmp  23438  cldllycmp  23439  lly1stc  23440  dislly  23441  llycmpkgen2  23494  1stckgenlem  23497  txlly  23580  txnlly  23581  txtube  23584  txcmplem1  23585  txcmplem2  23586  xkococnlem  23603  basqtop  23655  tgqtop  23656  infil  23807  fmfnfmlem4  23901  hauspwpwf1  23931  tgpconncompss  24058  ustfilxp  24157  metrest  24468  tgioo  24740  zdis  24761  icccmplem1  24767  icccmplem2  24768  reconnlem2  24772  xrge0tsms  24779  cnheibor  24910  cnllycmp  24911  ncvs1  25113  cphsqrtcl  25140  cmetcaulem  25244  ovollb2lem  25445  ovolctb  25447  ovolshftlem1  25466  ovolscalem1  25470  ovolicc1  25473  ioombl1lem1  25515  ioorf  25530  ioorcl  25534  dyadf  25548  vitalilem2  25566  vitali  25570  i1faddlem  25650  i1fmullem  25651  dvres2lem  25867  dvaddbr  25896  dvmulbr  25897  dvmulbrOLD  25898  lhop1lem  25974  lhop  25977  dvcnvrelem2  25979  ig1peu  26136  tayl0  26325  rlimcnp2  26932  xrlimcnp  26934  ppisval  27070  ppisval2  27071  ppinprm  27118  chtnprm  27120  2sqlem7  27391  chebbnd1lem1  27436  footexALT  28790  footexlem2  28792  foot  28794  footne  28795  perprag  28798  colperpexlem3  28804  mideulem2  28806  lnopp2hpgb  28835  colopp  28841  lmieu  28856  lmimid  28866  hypcgrlem1  28871  hypcgrlem2  28872  trgcopyeulem  28877  f1otrg  28943  eengtrkg  29059  shuni  31375  5oalem1  31729  5oalem2  31730  5oalem4  31732  5oalem5  31733  3oalem2  31738  pjclem4  32274  pj3si  32282  ccatf1  33031  xrge0tsmsd  33155  wrdpmtrlast  33175  idlinsubrg  33512  ssdifidlprm  33539  qsdrngilem  33575  qsdrngi  33576  pidufd  33624  exsslsb  33753  lindsunlem  33781  lbsdiflsp0  33783  dimkerim  33784  irngss  33844  cmpcref  34007  cmppcmp  34015  dispcmp  34016  zarcmplem  34038  prsdm  34071  prsrn  34072  pnfneige0  34108  qqhucn  34149  rrhqima  34171  gsumesum  34216  esumcst  34220  esum2d  34250  sigainb  34293  inelpisys  34311  dynkin  34324  eulerpartlemgh  34535  eulerpartlemgs2  34537  eulerpartlemn  34538  sseqmw  34548  sseqf  34549  sseqp1  34552  fibp1  34558  bnj1379  34986  bnj1177  35162  cnllysconn  35439  rellysconn  35445  cvmsss2  35468  cvmcov2  35469  cvmopnlem  35472  mclsind  35764  weiunfr  36661  poimirlem30  37851  blbnd  37988  ssbnd  37989  heiborlem1  38012  heiborlem8  38019  heibor  38022  mndomgmid  38072  pmodlem1  40106  pclfinN  40160  mapdunirnN  41910  hdmaprnlem9N  42117  mhpind  42837  elrfi  42936  elrfirn  42937  fnwe2lem2  43293  dfac11  43304  kelac1  43305  kelac2lem  43306  dfac21  43308  islssfgi  43314  filnm  43332  lpirlnr  43359  hbtlem6  43371  hbt  43372  iocinico  43454  restuni3  45362  disjinfi  45436  iooabslt  45745  iocopn  45766  icoopn  45771  uzinico  45805  limciccioolb  45867  limcicciooub  45881  islpcn  45883  limcresioolb  45887  limcleqr  45888  limsuppnfdlem  45945  limsupresxr  46010  liminfresxr  46011  liminfvalxr  46027  liminflelimsupuz  46029  cnrefiisplem  46073  ioccncflimc  46129  icccncfext  46131  icocncflimc  46133  cncfiooicclem1  46137  itgiccshift  46224  itgperiod  46225  itgsbtaddcnst  46226  stoweidlem57  46301  fourierdlem20  46371  fourierdlem32  46383  fourierdlem33  46384  fourierdlem48  46398  fourierdlem49  46399  fourierdlem62  46412  fourierdlem71  46421  fouriersw  46475  qndenserrnbllem  46538  qndenserrn  46543  salgencntex  46587  fsumlesge0  46621  sge0tsms  46624  sge0cl  46625  sge0f1o  46626  sge0sup  46635  sge0resplit  46650  sge0iunmptlemre  46659  sge0fodjrnlem  46660  sge0rpcpnf  46665  sge0xaddlem1  46677  ovolval4lem2  46894  sssmf  46982  smflimlem3  47017  smfsuplem1  47055  fcores  47313  prproropf1olem2  47750  iinfconstbaslem  49310  ffthoppf  49410  uobeqw  49464  uobeq  49465  swapfiso  49530  swapciso  49531  fucoppcffth  49656  thincciso  49698  thinccisod  49699  termcterm  49758  termcterm2  49759  termcterm3  49760  termcciso  49761  termc2  49763  diagciso  49784  diagcic  49785  uobeqterm  49791