Theorem elind 3688

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 3687	. 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 1767   i^i cin 3475

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1601  ax-4 1612  ax-5 1680  ax-6 1719  ax-7 1739  ax-10 1786  ax-11 1791  ax-12 1803  ax-13 1968  ax-ext 2445

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1382  df-ex 1597  df-nf 1600  df-sb 1712  df-clab 2453  df-cleq 2459  df-clel 2462  df-nfc 2617  df-v 3115  df-in 3483

This theorem is referenced by:  tfrlem5  7049  uniinqs  7391  unifpw  7822  f1opwfi  7823  fissuni  7824  fipreima  7825  elfir  7874  inelfi  7877  cantnfcl  8085  cantnfclOLD  8115  tskwe  8330  infpwfidom  8408  infpwfien  8442  ackbij2lem1  8598  ackbij1lem3  8601  ackbij1lem4  8602  ackbij1lem6  8604  ackbij1lem11  8609  fin23lem24  8701  isfin1-3  8765  fpwwe2lem12  9018  fpwwe  9023  canthnumlem  9025  fz1isolem  12475  strfv2d  14521  submre  14859  submrc  14882  isacs2  14907  coffth  15162  catcoppccl  15292  catcfuccl  15293  catcxpccl  15333  isdrs2  15425  fpwipodrs  15650  sylow2a  16442  lsmmod  16496  lsmdisj  16502  lsmdisj2  16503  subgdisj1  16512  frgpnabllem1  16677  dmdprdd  16830  dprdfeq0  16861  dprdfeq0OLD  16868  dprdres  16874  dprddisj2  16886  dprddisj2OLD  16887  dprd2da  16890  dmdprdsplit2lem  16893  ablfacrp  16916  pgpfac1lem3a  16926  pgpfac1lem3  16927  pgpfaclem1  16931  aspval  17764  mplind  17954  zringlpirlem1  18292  zringlpirlem3  18294  zlpirlem1  18297  zlpirlem3  18299  pmatcoe1fsupp  18985  baspartn  19238  bastg  19250  clsval2  19333  isopn3  19349  restbas  19441  lmss  19581  cmpcovf  19673  discmp  19680  cmpsublem  19681  cmpsub  19682  iscon2  19697  conclo  19698  llynlly  19760  restnlly  19765  restlly  19766  islly2  19767  llyrest  19768  nllyrest  19769  llyidm  19771  nllyidm  19772  hausllycmp  19777  cldllycmp  19778  lly1stc  19779  dislly  19780  llycmpkgen2  19802  1stckgenlem  19805  txlly  19888  txnlly  19889  txtube  19892  txcmplem1  19893  txcmplem2  19894  xkococnlem  19911  basqtop  19963  tgqtop  19964  infil  20115  fmfnfmlem4  20209  hauspwpwf1  20239  tgpconcompss  20363  ustfilxp  20466  metrest  20778  tgioo  21052  zdis  21072  icccmplem1  21078  icccmplem2  21079  reconnlem2  21083  xrge0tsms  21090  cnheibor  21206  cnllycmp  21207  cphsqrtcl  21382  cmetcaulem  21478  ovollb2lem  21650  ovolctb  21652  ovolshftlem1  21671  ovolscalem1  21675  ovolicc1  21678  ioombl1lem1  21719  ioorf  21733  ioorcl  21737  dyadf  21751  vitalilem2  21769  vitali  21773  i1faddlem  21851  dvres2lem  22065  dvaddbr  22092  dvmulbr  22093  lhop1lem  22165  lhop  22168  dvcnvrelem2  22170  ig1peu  22323  tayl0  22507  rlimcnp2  23040  xrlimcnp  23042  ppisval  23121  ppisval2  23122  ppinprm  23170  chtnprm  23172  2sqlem7  23389  chebbnd1lem1  23398  foot  23820  perprag  23821  colperpexlem3  23827  mideulem  23829  lmieu  23843  lmimid  23852  hypcgrlem1  23857  hypcgrlem2  23858  f1otrg  23866  eengtrkg  23980  mndomgmid  25036  shuni  25910  5oalem1  26264  5oalem2  26265  5oalem4  26267  5oalem5  26268  3oalem2  26273  pjclem4  26810  pj3si  26818  xrge0tsmsd  27454  prsdm  27548  prsrn  27549  pnfneige0  27585  qqhucn  27625  gsumesum  27723  esumcst  27727  sigainb  27792  eulerpartlemgh  27973  eulerpartlemgs2  27975  eulerpartlemn  27976  sseqmw  27986  sseqf  27987  sseqp1  27990  fibp1  27996  cnllyscon  28346  rellyscon  28352  cvmsss2  28375  cvmcov2  28376  cvmopnlem  28379  blbnd  29902  ssbnd  29903  heiborlem1  29926  heiborlem8  29933  heibor  29936  elrfi  30246  elrfirn  30247  fnwe2lem2  30617  dfac11  30628  kelac1  30629  kelac2lem  30630  dfac21  30632  islssfgi  30638  filnm  30656  lpirlnr  30686  hbtlem6  30698  hbt  30699  cntzsdrg  30772  iocinico  30800  isprm7  30811  iooabslt  31112  iocopn  31140  icoopn  31145  islpcn  31197  limcresioolb  31201  limcleqr  31202  ioccncflimc  31240  icocncflimc  31244  stoweidlem57  31373  fourierdlem71  31494  fouriersw  31548  bnj1379  32977  bnj1177  33150  pmodlem1  34651  pclfinN  34705  mapdunirnN  36456  hdmaprnlem9N  36666