Theorem elind 3650

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 3649	. 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 1872   i^i cin 3435

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1663  ax-4 1676  ax-5 1752  ax-6 1798  ax-7 1843  ax-10 1891  ax-11 1896  ax-12 1909  ax-13 2057  ax-ext 2401

This theorem depends on definitions:  df-bi 188  df-an 372  df-tru 1440  df-ex 1658  df-nf 1662  df-sb 1791  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2568  df-v 3082  df-in 3443

This theorem is referenced by:  tfrlem5  7109  uniinqs  7454  unifpw  7886  f1opwfi  7887  fissuni  7888  fipreima  7889  elfir  7938  inelfi  7941  cantnfcl  8180  tskwe  8392  infpwfidom  8466  infpwfien  8500  ackbij2lem1  8656  ackbij1lem3  8659  ackbij1lem4  8660  ackbij1lem6  8662  ackbij1lem11  8667  fin23lem24  8759  isfin1-3  8823  fpwwe2lem12  9073  fpwwe  9078  canthnumlem  9080  fz1isolem  12628  strfv2d  15154  submre  15510  submrc  15533  isacs2  15558  coffth  15840  catcoppccl  16002  catcfuccl  16003  catcxpccl  16091  isdrs2  16183  fpwipodrs  16409  sylow2a  17270  lsmmod  17324  lsmdisj  17330  lsmdisj2  17331  subgdisj1  17340  frgpnabllem1  17508  dmdprdd  17630  dprdfeq0  17654  dprdres  17660  dprddisj2  17671  dprd2da  17674  dmdprdsplit2lem  17677  ablfacrp  17698  pgpfac1lem3a  17708  pgpfac1lem3  17709  pgpfaclem1  17713  aspval  18551  mplind  18724  zringlpirlem1  19051  zringlpirlem3OLD  19053  zringlpirlem3  19055  pmatcoe1fsupp  19723  baspartn  19967  bastg  19979  clsval2  20063  isopn3  20080  restbas  20172  lmss  20312  cmpcovf  20404  discmp  20411  cmpsublem  20412  cmpsub  20413  iscon2  20427  conclo  20428  llynlly  20490  restnlly  20495  restlly  20496  islly2  20497  llyrest  20498  nllyrest  20499  llyidm  20501  nllyidm  20502  hausllycmp  20507  cldllycmp  20508  lly1stc  20509  dislly  20510  llycmpkgen2  20563  1stckgenlem  20566  txlly  20649  txnlly  20650  txtube  20653  txcmplem1  20654  txcmplem2  20655  xkococnlem  20672  basqtop  20724  tgqtop  20725  infil  20876  fmfnfmlem4  20970  hauspwpwf1  21000  tgpconcompss  21126  ustfilxp  21225  metrest  21537  tgioo  21812  zdis  21832  icccmplem1  21838  icccmplem2  21839  reconnlem2  21843  xrge0tsms  21850  cnheibor  21981  cnllycmp  21982  cphsqrtcl  22160  cmetcaulem  22256  ovollb2lem  22439  ovolctb  22441  ovolshftlem1  22460  ovolscalem1  22464  ovolicc1  22467  ioombl1lem1  22509  ioorf  22523  ioorcl  22527  ioorfOLD  22528  ioorclOLD  22532  dyadf  22547  vitalilem2  22565  vitali  22569  i1faddlem  22649  dvres2lem  22863  dvaddbr  22890  dvmulbr  22891  lhop1lem  22963  lhop  22966  dvcnvrelem2  22968  ig1peu  23120  ig1peuOLD  23121  tayl0  23315  rlimcnp2  23890  xrlimcnp  23892  ppisval  24028  ppisval2  24029  ppinprm  24077  chtnprm  24079  2sqlem7  24296  chebbnd1lem1  24305  footex  24761  foot  24762  footne  24763  perprag  24766  colperpexlem3  24772  mideulem2  24774  lnopp2hpgb  24803  colopp  24809  lmieu  24824  lmimid  24834  hypcgrlem1  24839  hypcgrlem2  24840  trgcopyeulem  24845  f1otrg  24899  eengtrkg  25013  mndomgmid  26068  shuni  26951  5oalem1  27305  5oalem2  27306  5oalem4  27308  5oalem5  27309  3oalem2  27314  pjclem4  27850  pj3si  27858  xrge0tsmsd  28556  cmpcref  28685  cmppcmp  28693  dispcmp  28694  prsdm  28728  prsrn  28729  pnfneige0  28765  qqhucn  28804  rrhqima  28826  gsumesum  28888  esumcst  28892  esum2d  28922  sigainb  28966  inelpisys  28984  dynkin  28997  eulerpartlemgh  29219  eulerpartlemgs2  29221  eulerpartlemn  29222  sseqmw  29232  sseqf  29233  sseqp1  29236  fibp1  29242  bnj1379  29650  bnj1177  29823  cnllyscon  29976  rellyscon  29982  cvmsss2  30005  cvmcov2  30006  cvmopnlem  30009  mclsind  30216  poimirlem30  31934  blbnd  32083  ssbnd  32084  heiborlem1  32107  heiborlem8  32114  heibor  32117  pmodlem1  33380  pclfinN  33434  mapdunirnN  35187  hdmaprnlem9N  35397  elrfi  35505  elrfirn  35506  fnwe2lem2  35879  dfac11  35890  kelac1  35891  kelac2lem  35892  dfac21  35894  islssfgi  35900  filnm  35918  lpirlnr  35946  hbtlem6  35958  hbt  35959  cntzsdrg  36038  iocinico  36066  isprm7  36630  disjinfi  37429  iooabslt  37545  iocopn  37570  icoopn  37575  limciccioolb  37641  limcicciooub  37657  islpcn  37659  limcresioolb  37664  limcleqr  37665  ioccncflimc  37703  icccncfext  37705  icocncflimc  37707  cncfiooicclem1  37711  itgiccshift  37797  itgperiod  37798  itgsbtaddcnst  37799  stoweidlem57  37858  fourierdlem20  37929  fourierdlem32  37942  fourierdlem33  37943  fourierdlem48  37958  fourierdlem49  37959  fourierdlem62  37972  fourierdlem71  37981  fouriersw  38035  fsumlesge0  38127  sge0tsms  38130  sge0cl  38131  sge0f1o  38132  sge0sup  38141  sge0resplit  38156  sge0iunmptlemre  38165  sge0fodjrnlem  38166  sge0rpcpnf  38171  sge0xaddlem1  38183  zrinitorngc  39621  zrtermorngc  39622  zrzeroorngc  39623  irinitoringc  39690  zrtermoringc  39691  zrninitoringc  39692  nzerooringczr  39693