Theorem elind 3674

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

Syntax hints:   -> wi 4   e. wcel 1823   i^i cin 3460

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1623  ax-4 1636  ax-5 1709  ax-6 1752  ax-7 1795  ax-10 1842  ax-11 1847  ax-12 1859  ax-13 2004  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 369  df-tru 1401  df-ex 1618  df-nf 1622  df-sb 1745  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3108  df-in 3468

This theorem is referenced by:  tfrlem5  7041  uniinqs  7383  unifpw  7815  f1opwfi  7816  fissuni  7817  fipreima  7818  elfir  7867  inelfi  7870  cantnfcl  8077  cantnfclOLD  8107  tskwe  8322  infpwfidom  8400  infpwfien  8434  ackbij2lem1  8590  ackbij1lem3  8593  ackbij1lem4  8594  ackbij1lem6  8596  ackbij1lem11  8601  fin23lem24  8693  isfin1-3  8757  fpwwe2lem12  9008  fpwwe  9013  canthnumlem  9015  fz1isolem  12494  strfv2d  14750  submre  15094  submrc  15117  isacs2  15142  coffth  15424  catcoppccl  15586  catcfuccl  15587  catcxpccl  15675  isdrs2  15767  fpwipodrs  15993  sylow2a  16838  lsmmod  16892  lsmdisj  16898  lsmdisj2  16899  subgdisj1  16908  frgpnabllem1  17076  dmdprdd  17225  dprdfeq0  17257  dprdfeq0OLD  17264  dprdres  17270  dprddisj2  17282  dprddisj2OLD  17283  dprd2da  17286  dmdprdsplit2lem  17289  ablfacrp  17312  pgpfac1lem3a  17322  pgpfac1lem3  17323  pgpfaclem1  17327  aspval  18172  mplind  18362  zringlpirlem1  18697  zringlpirlem3  18699  pmatcoe1fsupp  19369  baspartn  19622  bastg  19634  clsval2  19718  isopn3  19734  restbas  19826  lmss  19966  cmpcovf  20058  discmp  20065  cmpsublem  20066  cmpsub  20067  iscon2  20081  conclo  20082  llynlly  20144  restnlly  20149  restlly  20150  islly2  20151  llyrest  20152  nllyrest  20153  llyidm  20155  nllyidm  20156  hausllycmp  20161  cldllycmp  20162  lly1stc  20163  dislly  20164  llycmpkgen2  20217  1stckgenlem  20220  txlly  20303  txnlly  20304  txtube  20307  txcmplem1  20308  txcmplem2  20309  xkococnlem  20326  basqtop  20378  tgqtop  20379  infil  20530  fmfnfmlem4  20624  hauspwpwf1  20654  tgpconcompss  20778  ustfilxp  20881  metrest  21193  tgioo  21467  zdis  21487  icccmplem1  21493  icccmplem2  21494  reconnlem2  21498  xrge0tsms  21505  cnheibor  21621  cnllycmp  21622  cphsqrtcl  21797  cmetcaulem  21893  ovollb2lem  22065  ovolctb  22067  ovolshftlem1  22086  ovolscalem1  22090  ovolicc1  22093  ioombl1lem1  22134  ioorf  22148  ioorcl  22152  dyadf  22166  vitalilem2  22184  vitali  22188  i1faddlem  22266  dvres2lem  22480  dvaddbr  22507  dvmulbr  22508  lhop1lem  22580  lhop  22583  dvcnvrelem2  22585  ig1peu  22738  tayl0  22923  rlimcnp2  23494  xrlimcnp  23496  ppisval  23575  ppisval2  23576  ppinprm  23624  chtnprm  23626  2sqlem7  23843  chebbnd1lem1  23852  footex  24296  foot  24297  footne  24298  perprag  24301  colperpexlem3  24307  mideulem2  24309  lnopp2hpgb  24333  lmieu  24351  lmimid  24360  hypcgrlem1  24365  hypcgrlem2  24366  f1otrg  24376  eengtrkg  24490  mndomgmid  25542  shuni  26416  5oalem1  26770  5oalem2  26771  5oalem4  26773  5oalem5  26774  3oalem2  26779  pjclem4  27316  pj3si  27324  xrge0tsmsd  28010  cmpcref  28088  cmppcmp  28096  dispcmp  28097  prsdm  28131  prsrn  28132  pnfneige0  28168  qqhucn  28207  gsumesum  28288  esumcst  28292  esum2d  28322  sigainb  28366  eulerpartlemgh  28581  eulerpartlemgs2  28583  eulerpartlemn  28584  sseqmw  28594  sseqf  28595  sseqp1  28598  fibp1  28604  cnllyscon  28954  rellyscon  28960  cvmsss2  28983  cvmcov2  28984  cvmopnlem  28987  mclsind  29194  blbnd  30523  ssbnd  30524  heiborlem1  30547  heiborlem8  30554  heibor  30557  elrfi  30866  elrfirn  30867  fnwe2lem2  31236  dfac11  31247  kelac1  31248  kelac2lem  31249  dfac21  31251  islssfgi  31257  filnm  31275  lpirlnr  31307  hbtlem6  31319  hbt  31320  cntzsdrg  31392  iocinico  31420  isprm7  31433  iooabslt  31771  iocopn  31799  icoopn  31804  limciccioolb  31866  limcicciooub  31882  islpcn  31884  limcresioolb  31888  limcleqr  31889  ioccncflimc  31927  icccncfext  31929  icocncflimc  31931  cncfiooicclem1  31935  itgiccshift  32018  itgperiod  32019  itgsbtaddcnst  32020  stoweidlem57  32078  fourierdlem20  32148  fourierdlem32  32160  fourierdlem33  32161  fourierdlem48  32176  fourierdlem49  32177  fourierdlem62  32190  fourierdlem71  32199  fouriersw  32253  zrinitorngc  33062  zrtermorngc  33063  zrzeroorngc  33064  irinitoringc  33131  zrtermoringc  33132  zrninitoringc  33133  nzerooringczr  33134  bnj1379  34290  bnj1177  34463  pmodlem1  35967  pclfinN  36021  mapdunirnN  37774  hdmaprnlem9N  37984