Theorem elind 3586

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
elind.1	|- ( ph -> X e. A )
elind.2	|- ( ph -> X e. B )

Assertion

Ref	Expression
elind	|- ( ph -> X e. ( A i^i B ) )

Proof of Theorem elind

Step	Hyp	Ref	Expression
1		elind.1	. 2 |- ( ph -> X e. A )
2		elind.2	. 2 |- ( ph -> X e. B )
3		elin 3585	. 2 |- ( X e. ( A i^i B ) <-> ( X e. A /\ X e. B ) )
4	1, 2, 3	sylanbrc 675	1 |- ( ph -> X e. ( A i^i B ) )

Syntax hints:   -> wi 4   e. wcel 1891   i^i cin 3371

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1673  ax-4 1686  ax-5 1762  ax-6 1809  ax-7 1855  ax-10 1919  ax-11 1924  ax-12 1937  ax-13 2092  ax-ext 2432

This theorem depends on definitions:  df-bi 190  df-an 377  df-tru 1451  df-ex 1668  df-nf 1672  df-sb 1802  df-clab 2439  df-cleq 2445  df-clel 2448  df-nfc 2582  df-v 3015  df-in 3379

This theorem is referenced by:  tfrlem5  7085  uniinqs  7430  unifpw  7864  f1opwfi  7865  fissuni  7866  fipreima  7867  elfir  7916  inelfi  7919  cantnfcl  8159  tskwe  8371  infpwfidom  8446  infpwfien  8480  ackbij2lem1  8636  ackbij1lem3  8639  ackbij1lem4  8640  ackbij1lem6  8642  ackbij1lem11  8647  fin23lem24  8739  isfin1-3  8803  fpwwe2lem12  9053  fpwwe  9058  canthnumlem  9060  fz1isolem  12619  strfv2d  15166  submre  15522  submrc  15545  isacs2  15570  coffth  15852  catcoppccl  16014  catcfuccl  16015  catcxpccl  16103  isdrs2  16195  fpwipodrs  16421  sylow2a  17282  lsmmod  17336  lsmdisj  17342  lsmdisj2  17343  subgdisj1  17352  frgpnabllem1  17520  dmdprdd  17642  dprdfeq0  17666  dprdres  17672  dprddisj2  17683  dprd2da  17686  dmdprdsplit2lem  17689  ablfacrp  17710  pgpfac1lem3a  17720  pgpfac1lem3  17721  pgpfaclem1  17725  aspval  18563  mplind  18736  zringlpirlem1  19064  zringlpirlem3OLD  19066  zringlpirlem3  19068  pmatcoe1fsupp  19736  baspartn  19980  bastg  19992  clsval2  20076  isopn3  20093  restbas  20185  lmss  20325  cmpcovf  20417  discmp  20424  cmpsublem  20425  cmpsub  20426  iscon2  20440  conclo  20441  llynlly  20503  restnlly  20508  restlly  20509  islly2  20510  llyrest  20511  nllyrest  20512  llyidm  20514  nllyidm  20515  hausllycmp  20520  cldllycmp  20521  lly1stc  20522  dislly  20523  llycmpkgen2  20576  1stckgenlem  20579  txlly  20662  txnlly  20663  txtube  20666  txcmplem1  20667  txcmplem2  20668  xkococnlem  20685  basqtop  20737  tgqtop  20738  infil  20889  fmfnfmlem4  20983  hauspwpwf1  21013  tgpconcompss  21139  ustfilxp  21238  metrest  21550  tgioo  21825  zdis  21845  icccmplem1  21851  icccmplem2  21852  reconnlem2  21856  xrge0tsms  21863  cnheibor  21994  cnllycmp  21995  cphsqrtcl  22173  cmetcaulem  22269  ovollb2lem  22452  ovolctb  22454  ovolshftlem1  22473  ovolscalem1  22477  ovolicc1  22480  ioombl1lem1  22523  ioorf  22537  ioorcl  22541  ioorfOLD  22542  ioorclOLD  22546  dyadf  22561  vitalilem2  22579  vitali  22583  i1faddlem  22663  dvres2lem  22877  dvaddbr  22904  dvmulbr  22905  lhop1lem  22977  lhop  22980  dvcnvrelem2  22982  ig1peu  23134  ig1peuOLD  23135  tayl0  23329  rlimcnp2  23904  xrlimcnp  23906  ppisval  24042  ppisval2  24043  ppinprm  24091  chtnprm  24093  2sqlem7  24310  chebbnd1lem1  24319  footex  24775  foot  24776  footne  24777  perprag  24780  colperpexlem3  24786  mideulem2  24788  lnopp2hpgb  24817  colopp  24823  lmieu  24838  lmimid  24848  hypcgrlem1  24853  hypcgrlem2  24854  trgcopyeulem  24859  f1otrg  24913  eengtrkg  25027  mndomgmid  26082  shuni  26965  5oalem1  27319  5oalem2  27320  5oalem4  27322  5oalem5  27323  3oalem2  27328  pjclem4  27864  pj3si  27872  xrge0tsmsd  28555  cmpcref  28684  cmppcmp  28692  dispcmp  28693  prsdm  28727  prsrn  28728  pnfneige0  28764  qqhucn  28803  rrhqima  28825  gsumesum  28887  esumcst  28891  esum2d  28921  sigainb  28965  inelpisys  28983  dynkin  28996  eulerpartlemgh  29217  eulerpartlemgs2  29219  eulerpartlemn  29220  sseqmw  29230  sseqf  29231  sseqp1  29234  fibp1  29240  bnj1379  29648  bnj1177  29821  cnllyscon  29974  rellyscon  29980  cvmsss2  30003  cvmcov2  30004  cvmopnlem  30007  mclsind  30214  poimirlem30  31972  blbnd  32121  ssbnd  32122  heiborlem1  32145  heiborlem8  32152  heibor  32155  pmodlem1  33413  pclfinN  33467  mapdunirnN  35220  hdmaprnlem9N  35430  elrfi  35538  elrfirn  35539  fnwe2lem2  35911  dfac11  35922  kelac1  35923  kelac2lem  35924  dfac21  35926  islssfgi  35932  filnm  35950  lpirlnr  35978  hbtlem6  35990  hbt  35991  cntzsdrg  36070  iocinico  36098  isprm7  36661  disjinfi  37478  iooabslt  37637  iocopn  37662  icoopn  37667  limciccioolb  37743  limcicciooub  37759  islpcn  37761  limcresioolb  37766  limcleqr  37767  ioccncflimc  37805  icccncfext  37807  icocncflimc  37809  cncfiooicclem1  37813  itgiccshift  37899  itgperiod  37900  itgsbtaddcnst  37901  stoweidlem57  37975  fourierdlem20  38046  fourierdlem32  38059  fourierdlem33  38060  fourierdlem48  38075  fourierdlem49  38076  fourierdlem62  38089  fourierdlem71  38098  fouriersw  38152  qndenserrnbllem  38220  qndenserrn  38225  salgencntex  38259  fsumlesge0  38278  sge0tsms  38281  sge0cl  38282  sge0f1o  38283  sge0sup  38292  sge0resplit  38307  sge0iunmptlemre  38316  sge0fodjrnlem  38317  sge0rpcpnf  38322  sge0xaddlem1  38334  ovolval4lem2  38535  zrinitorngc  40327  zrtermorngc  40328  zrzeroorngc  40329  irinitoringc  40396  zrtermoringc  40397  zrninitoringc  40398  nzerooringczr  40399