Theorem elind 3656

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 3655	. 2 |- ( X e. ( A i^i B ) <-> ( X e. A /\ X e. B ) )
4	1, 2, 3	sylanbrc 668	1 |- ( ph -> X e. ( A i^i B ) )

Syntax hints:   -> wi 4   e. wcel 1870   i^i cin 3441

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1751  ax-6 1797  ax-7 1841  ax-10 1889  ax-11 1894  ax-12 1907  ax-13 2055  ax-ext 2407

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1790  df-clab 2415  df-cleq 2421  df-clel 2424  df-nfc 2579  df-v 3089  df-in 3449

This theorem is referenced by:  tfrlem5  7106  uniinqs  7451  unifpw  7883  f1opwfi  7884  fissuni  7885  fipreima  7886  elfir  7935  inelfi  7938  cantnfcl  8171  tskwe  8383  infpwfidom  8457  infpwfien  8491  ackbij2lem1  8647  ackbij1lem3  8650  ackbij1lem4  8651  ackbij1lem6  8653  ackbij1lem11  8658  fin23lem24  8750  isfin1-3  8814  fpwwe2lem12  9065  fpwwe  9070  canthnumlem  9072  fz1isolem  12619  strfv2d  15118  submre  15462  submrc  15485  isacs2  15510  coffth  15792  catcoppccl  15954  catcfuccl  15955  catcxpccl  16043  isdrs2  16135  fpwipodrs  16361  sylow2a  17206  lsmmod  17260  lsmdisj  17266  lsmdisj2  17267  subgdisj1  17276  frgpnabllem1  17444  dmdprdd  17566  dprdfeq0  17590  dprdres  17596  dprddisj2  17607  dprd2da  17610  dmdprdsplit2lem  17613  ablfacrp  17634  pgpfac1lem3a  17644  pgpfac1lem3  17645  pgpfaclem1  17649  aspval  18487  mplind  18660  zringlpirlem1  18987  zringlpirlem3  18989  pmatcoe1fsupp  19656  baspartn  19900  bastg  19912  clsval2  19996  isopn3  20013  restbas  20105  lmss  20245  cmpcovf  20337  discmp  20344  cmpsublem  20345  cmpsub  20346  iscon2  20360  conclo  20361  llynlly  20423  restnlly  20428  restlly  20429  islly2  20430  llyrest  20431  nllyrest  20432  llyidm  20434  nllyidm  20435  hausllycmp  20440  cldllycmp  20441  lly1stc  20442  dislly  20443  llycmpkgen2  20496  1stckgenlem  20499  txlly  20582  txnlly  20583  txtube  20586  txcmplem1  20587  txcmplem2  20588  xkococnlem  20605  basqtop  20657  tgqtop  20658  infil  20809  fmfnfmlem4  20903  hauspwpwf1  20933  tgpconcompss  21059  ustfilxp  21158  metrest  21470  tgioo  21725  zdis  21745  icccmplem1  21751  icccmplem2  21752  reconnlem2  21756  xrge0tsms  21763  cnheibor  21879  cnllycmp  21880  cphsqrtcl  22055  cmetcaulem  22151  ovollb2lem  22319  ovolctb  22321  ovolshftlem1  22340  ovolscalem1  22344  ovolicc1  22347  ioombl1lem1  22388  ioorf  22402  ioorcl  22406  ioorfOLD  22407  ioorclOLD  22411  dyadf  22426  vitalilem2  22444  vitali  22448  i1faddlem  22528  dvres2lem  22742  dvaddbr  22769  dvmulbr  22770  lhop1lem  22842  lhop  22845  dvcnvrelem2  22847  ig1peu  22997  tayl0  23182  rlimcnp2  23757  xrlimcnp  23759  ppisval  23893  ppisval2  23894  ppinprm  23942  chtnprm  23944  2sqlem7  24161  chebbnd1lem1  24170  footex  24620  foot  24621  footne  24622  perprag  24625  colperpexlem3  24631  mideulem2  24633  lnopp2hpgb  24661  colopp  24667  lmieu  24682  lmimid  24692  hypcgrlem1  24697  hypcgrlem2  24698  trgcopyeulem  24703  f1otrg  24747  eengtrkg  24861  mndomgmid  25915  shuni  26788  5oalem1  27142  5oalem2  27143  5oalem4  27145  5oalem5  27146  3oalem2  27151  pjclem4  27687  pj3si  27695  xrge0tsmsd  28387  cmpcref  28516  cmppcmp  28524  dispcmp  28525  prsdm  28559  prsrn  28560  pnfneige0  28596  qqhucn  28635  rrhqima  28657  gsumesum  28719  esumcst  28723  esum2d  28753  sigainb  28797  inelpisys  28815  dynkin  28828  eulerpartlemgh  29037  eulerpartlemgs2  29039  eulerpartlemn  29040  sseqmw  29050  sseqf  29051  sseqp1  29054  fibp1  29060  bnj1379  29430  bnj1177  29603  cnllyscon  29756  rellyscon  29762  cvmsss2  29785  cvmcov2  29786  cvmopnlem  29789  mclsind  29996  poimirlem30  31674  blbnd  31823  ssbnd  31824  heiborlem1  31847  heiborlem8  31854  heibor  31857  pmodlem1  33120  pclfinN  33174  mapdunirnN  34927  hdmaprnlem9N  35137  elrfi  35245  elrfirn  35246  fnwe2lem2  35615  dfac11  35626  kelac1  35627  kelac2lem  35628  dfac21  35630  islssfgi  35636  filnm  35654  lpirlnr  35682  hbtlem6  35694  hbt  35695  cntzsdrg  35767  iocinico  35795  isprm7  36297  disjinfi  37091  iooabslt  37181  iocopn  37206  icoopn  37211  limciccioolb  37273  limcicciooub  37289  islpcn  37291  limcresioolb  37296  limcleqr  37297  ioccncflimc  37335  icccncfext  37337  icocncflimc  37339  cncfiooicclem1  37343  itgiccshift  37426  itgperiod  37427  itgsbtaddcnst  37428  stoweidlem57  37487  fourierdlem20  37558  fourierdlem32  37570  fourierdlem33  37571  fourierdlem48  37586  fourierdlem49  37587  fourierdlem62  37600  fourierdlem71  37609  fouriersw  37663  fsumlesge0  37753  sge0tsms  37756  sge0cl  37757  sge0f1o  37758  sge0sup  37767  sge0resplit  37782  sge0iunmptlemre  37791  sge0fodjrnlem  37792  zrinitorngc  38760  zrtermorngc  38761  zrzeroorngc  38762  irinitoringc  38829  zrtermoringc  38830  zrninitoringc  38831  nzerooringczr  38832