Theorem elind 3798

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

Syntax hints:   -> wi 4   e. wcel 1990   i^i cin 3573

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1722  ax-4 1737  ax-5 1839  ax-6 1888  ax-7 1935  ax-9 1999  ax-10 2019  ax-11 2034  ax-12 2047  ax-13 2246  ax-ext 2602

This theorem depends on definitions:  df-bi 197  df-or 385  df-an 386  df-tru 1486  df-ex 1705  df-nf 1710  df-sb 1881  df-clab 2609  df-cleq 2615  df-clel 2618  df-nfc 2753  df-v 3202  df-in 3581

This theorem is referenced by:  tfrlem5  7476  uniinqs  7827  unifpw  8269  f1opwfi  8270  fissuni  8271  fipreima  8272  elfir  8321  inelfi  8324  cantnfcl  8564  tskwe  8776  infpwfidom  8851  infpwfien  8885  ackbij2lem1  9041  ackbij1lem3  9044  ackbij1lem4  9045  ackbij1lem6  9047  ackbij1lem11  9052  fin23lem24  9144  isfin1-3  9208  fpwwe2lem12  9463  fpwwe  9468  canthnumlem  9470  fz1isolem  13245  isprm7  15420  setsstruct2  15896  strfv2d  15905  submre  16265  submrc  16288  isacs2  16314  coffth  16596  catcoppccl  16758  catcfuccl  16759  catcxpccl  16847  isdrs2  16939  fpwipodrs  17164  sylow2a  18034  lsmmod  18088  lsmdisj  18094  lsmdisj2  18095  subgdisj1  18104  frgpnabllem1  18276  dmdprdd  18398  dprdfeq0  18421  dprdres  18427  dprddisj2  18438  dprd2da  18441  dmdprdsplit2lem  18444  ablfacrp  18465  pgpfac1lem3a  18475  pgpfac1lem3  18476  pgpfaclem1  18480  aspval  19328  mplind  19502  zringlpirlem1  19832  zringlpirlem3  19834  pmatcoe1fsupp  20506  baspartn  20758  bastg  20770  clsval2  20854  isopn3  20870  restbas  20962  lmss  21102  cmpcovf  21194  discmp  21201  cmpsublem  21202  cmpsub  21203  isconn2  21217  connclo  21218  llynlly  21280  restnlly  21285  restlly  21286  islly2  21287  llyrest  21288  nllyrest  21289  llyidm  21291  nllyidm  21292  hausllycmp  21297  cldllycmp  21298  lly1stc  21299  dislly  21300  llycmpkgen2  21353  1stckgenlem  21356  txlly  21439  txnlly  21440  txtube  21443  txcmplem1  21444  txcmplem2  21445  xkococnlem  21462  basqtop  21514  tgqtop  21515  infil  21667  fmfnfmlem4  21761  hauspwpwf1  21791  tgpconncompss  21917  ustfilxp  22016  metrest  22329  tgioo  22599  zdis  22619  icccmplem1  22625  icccmplem2  22626  reconnlem2  22630  xrge0tsms  22637  cnheibor  22754  cnllycmp  22755  ncvs1  22957  cphsqrtcl  22984  cmetcaulem  23086  ovollb2lem  23256  ovolctb  23258  ovolshftlem1  23277  ovolscalem1  23281  ovolicc1  23284  ioombl1lem1  23326  ioorf  23341  ioorcl  23345  dyadf  23359  vitalilem2  23378  vitali  23382  i1faddlem  23460  dvres2lem  23674  dvaddbr  23701  dvmulbr  23702  lhop1lem  23776  lhop  23779  dvcnvrelem2  23781  ig1peu  23931  tayl0  24116  rlimcnp2  24693  xrlimcnp  24695  ppisval  24830  ppisval2  24831  ppinprm  24878  chtnprm  24880  2sqlem7  25149  chebbnd1lem1  25158  footex  25613  foot  25614  footne  25615  perprag  25618  colperpexlem3  25624  mideulem2  25626  lnopp2hpgb  25655  colopp  25661  lmieu  25676  lmimid  25686  hypcgrlem1  25691  hypcgrlem2  25692  trgcopyeulem  25697  f1otrg  25751  eengtrkg  25865  wlkres  26567  shuni  28159  5oalem1  28513  5oalem2  28514  5oalem4  28516  5oalem5  28517  3oalem2  28522  pjclem4  29058  pj3si  29066  xrge0tsmsd  29785  cmpcref  29917  cmppcmp  29925  dispcmp  29926  prsdm  29960  prsrn  29961  pnfneige0  29997  qqhucn  30036  rrhqima  30058  gsumesum  30121  esumcst  30125  esum2d  30155  sigainb  30199  inelpisys  30217  dynkin  30230  eulerpartlemgh  30440  eulerpartlemgs2  30442  eulerpartlemn  30443  sseqmw  30453  sseqf  30454  sseqp1  30457  fibp1  30463  bnj1379  30901  bnj1177  31074  cnllysconn  31227  rellysconn  31233  cvmsss2  31256  cvmcov2  31257  cvmopnlem  31260  mclsind  31467  poimirlem30  33439  blbnd  33586  ssbnd  33587  heiborlem1  33610  heiborlem8  33617  heibor  33620  mndomgmid  33670  pmodlem1  35132  pclfinN  35186  mapdunirnN  36939  hdmaprnlem9N  37149  elrfi  37257  elrfirn  37258  fnwe2lem2  37621  dfac11  37632  kelac1  37633  kelac2lem  37634  dfac21  37636  islssfgi  37642  filnm  37660  lpirlnr  37687  hbtlem6  37699  hbt  37700  cntzsdrg  37772  iocinico  37797  restuni3  39301  disjinfi  39380  fvelimad  39458  fnfvimad  39459  fvelima2  39475  fnfvima2  39478  iooabslt  39721  iocopn  39746  icoopn  39751  uzinico  39787  limciccioolb  39853  limcicciooub  39869  islpcn  39871  limcresioolb  39875  limcleqr  39876  limsuppnfdlem  39933  limsupresxr  39998  liminfresxr  39999  liminfvalxr  40015  liminflelimsupuz  40017  cnrefiisplem  40055  ioccncflimc  40098  icccncfext  40100  icocncflimc  40102  cncfiooicclem1  40106  itgiccshift  40196  itgperiod  40197  itgsbtaddcnst  40198  stoweidlem57  40274  fourierdlem20  40344  fourierdlem32  40356  fourierdlem33  40357  fourierdlem48  40371  fourierdlem49  40372  fourierdlem62  40385  fourierdlem71  40394  fouriersw  40448  qndenserrnbllem  40514  qndenserrn  40519  salgencntex  40561  fsumlesge0  40594  sge0tsms  40597  sge0cl  40598  sge0f1o  40599  sge0sup  40608  sge0resplit  40623  sge0iunmptlemre  40632  sge0fodjrnlem  40633  sge0rpcpnf  40638  sge0xaddlem1  40650  ovolval4lem2  40864  sssmf  40947  smflimlem3  40981  smfsuplem1  41017  zrinitorngc  42000  zrtermorngc  42001  zrzeroorngc  42002  irinitoringc  42069  zrtermoringc  42070  zrninitoringc  42071  nzerooringczr  42072