Theorem elind 3535

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

Syntax hints:   -> wi 4   e. wcel 1756   i^i cin 3322

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2419

This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-clab 2425  df-cleq 2431  df-clel 2434  df-nfc 2563  df-v 2969  df-in 3330

This theorem is referenced by:  tfrlem5  6831  uniinqs  7172  unifpw  7606  f1opwfi  7607  fissuni  7608  fipreima  7609  elfir  7657  inelfi  7660  cantnfcl  7867  cantnfclOLD  7897  tskwe  8112  infpwfidom  8190  infpwfien  8224  ackbij2lem1  8380  ackbij1lem3  8383  ackbij1lem4  8384  ackbij1lem6  8386  ackbij1lem11  8391  fin23lem24  8483  isfin1-3  8547  fpwwe2lem12  8800  fpwwe  8805  canthnumlem  8807  fz1isolem  12206  strfv2d  14198  submre  14535  submrc  14558  isacs2  14583  coffth  14838  catcoppccl  14968  catcfuccl  14969  catcxpccl  15009  isdrs2  15101  fpwipodrs  15326  sylow2a  16109  lsmmod  16163  lsmdisj  16169  lsmdisj2  16170  subgdisj1  16179  frgpnabllem1  16342  dmdprdd  16469  dprdfeq0  16500  dprdfeq0OLD  16507  dprdres  16513  dprddisj2  16525  dprddisj2OLD  16526  dprd2da  16529  dmdprdsplit2lem  16532  ablfacrp  16555  pgpfac1lem3a  16565  pgpfac1lem3  16566  pgpfaclem1  16570  aspval  17376  mplind  17559  zringlpirlem1  17878  zringlpirlem3  17880  zlpirlem1  17883  zlpirlem3  17885  baspartn  18534  bastg  18546  clsval2  18629  isopn3  18645  restbas  18737  lmss  18877  cmpcovf  18969  discmp  18976  cmpsublem  18977  cmpsub  18978  iscon2  18993  conclo  18994  llynlly  19056  restnlly  19061  restlly  19062  islly2  19063  llyrest  19064  nllyrest  19065  llyidm  19067  nllyidm  19068  hausllycmp  19073  cldllycmp  19074  lly1stc  19075  dislly  19076  llycmpkgen2  19098  1stckgenlem  19101  txlly  19184  txnlly  19185  txtube  19188  txcmplem1  19189  txcmplem2  19190  xkococnlem  19207  basqtop  19259  tgqtop  19260  infil  19411  fmfnfmlem4  19505  hauspwpwf1  19535  tgpconcompss  19659  ustfilxp  19762  metrest  20074  tgioo  20348  zdis  20368  icccmplem1  20374  icccmplem2  20375  reconnlem2  20379  xrge0tsms  20386  cnheibor  20502  cnllycmp  20503  cphsqrcl  20678  cmetcaulem  20774  ovollb2lem  20946  ovolctb  20948  ovolshftlem1  20967  ovolscalem1  20971  ovolicc1  20974  ioombl1lem1  21014  ioorf  21028  ioorcl  21032  dyadf  21046  vitalilem2  21064  vitali  21068  i1faddlem  21146  dvres2lem  21360  dvaddbr  21387  dvmulbr  21388  lhop1lem  21460  lhop  21463  dvcnvrelem2  21465  ig1peu  21618  tayl0  21802  rlimcnp2  22335  xrlimcnp  22337  ppisval  22416  ppisval2  22417  ppinprm  22465  chtnprm  22467  2sqlem7  22684  chebbnd1lem1  22693  f1otrg  23068  eengtrkg  23182  mndomgmid  23780  shuni  24654  5oalem1  25008  5oalem2  25009  5oalem4  25011  5oalem5  25012  3oalem2  25017  pjclem4  25554  pj3si  25562  xrge0tsmsd  26204  prsdm  26296  prsrn  26297  pnfneige0  26333  qqhucn  26373  gsumesum  26462  esumcst  26466  sigainb  26531  eulerpartlemgh  26713  eulerpartlemgs2  26715  eulerpartlemn  26716  sseqmw  26726  sseqf  26727  sseqp1  26730  fibp1  26736  cnllyscon  27086  rellyscon  27092  cvmsss2  27115  cvmcov2  27116  cvmopnlem  27119  blbnd  28639  ssbnd  28640  heiborlem1  28663  heiborlem8  28670  heibor  28673  elrfi  28983  elrfirn  28984  fnwe2lem2  29357  dfac11  29368  kelac1  29369  kelac2lem  29370  dfac21  29372  islssfgi  29378  filnm  29396  lpirlnr  29426  hbtlem6  29438  hbt  29439  cntzsdrg  29512  iocinico  29540  stoweidlem57  29805  fsuppmapnn0fz  30746  pmatcollpw2lem  30820  bnj1379  31711  bnj1177  31884  pmodlem1  33330  pclfinN  33384  mapdunirnN  35135  hdmaprnlem9N  35345