Theorem elind 3651

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 3650	. 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 1758   i^i cin 3438

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1592  ax-4 1603  ax-5 1671  ax-6 1710  ax-7 1730  ax-10 1777  ax-11 1782  ax-12 1794  ax-13 1955  ax-ext 2432

This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1373  df-ex 1588  df-nf 1591  df-sb 1703  df-clab 2440  df-cleq 2446  df-clel 2449  df-nfc 2604  df-v 3080  df-in 3446

This theorem is referenced by:  tfrlem5  6952  uniinqs  7293  unifpw  7728  f1opwfi  7729  fissuni  7730  fipreima  7731  elfir  7779  inelfi  7782  cantnfcl  7989  cantnfclOLD  8019  tskwe  8234  infpwfidom  8312  infpwfien  8346  ackbij2lem1  8502  ackbij1lem3  8505  ackbij1lem4  8506  ackbij1lem6  8508  ackbij1lem11  8513  fin23lem24  8605  isfin1-3  8669  fpwwe2lem12  8922  fpwwe  8927  canthnumlem  8929  fz1isolem  12335  strfv2d  14327  submre  14665  submrc  14688  isacs2  14713  coffth  14968  catcoppccl  15098  catcfuccl  15099  catcxpccl  15139  isdrs2  15231  fpwipodrs  15456  sylow2a  16242  lsmmod  16296  lsmdisj  16302  lsmdisj2  16303  subgdisj1  16312  frgpnabllem1  16475  dmdprdd  16606  dprdfeq0  16637  dprdfeq0OLD  16644  dprdres  16650  dprddisj2  16662  dprddisj2OLD  16663  dprd2da  16666  dmdprdsplit2lem  16669  ablfacrp  16692  pgpfac1lem3a  16702  pgpfac1lem3  16703  pgpfaclem1  16707  aspval  17525  mplind  17711  zringlpirlem1  18031  zringlpirlem3  18033  zlpirlem1  18036  zlpirlem3  18038  baspartn  18694  bastg  18706  clsval2  18789  isopn3  18805  restbas  18897  lmss  19037  cmpcovf  19129  discmp  19136  cmpsublem  19137  cmpsub  19138  iscon2  19153  conclo  19154  llynlly  19216  restnlly  19221  restlly  19222  islly2  19223  llyrest  19224  nllyrest  19225  llyidm  19227  nllyidm  19228  hausllycmp  19233  cldllycmp  19234  lly1stc  19235  dislly  19236  llycmpkgen2  19258  1stckgenlem  19261  txlly  19344  txnlly  19345  txtube  19348  txcmplem1  19349  txcmplem2  19350  xkococnlem  19367  basqtop  19419  tgqtop  19420  infil  19571  fmfnfmlem4  19665  hauspwpwf1  19695  tgpconcompss  19819  ustfilxp  19922  metrest  20234  tgioo  20508  zdis  20528  icccmplem1  20534  icccmplem2  20535  reconnlem2  20539  xrge0tsms  20546  cnheibor  20662  cnllycmp  20663  cphsqrcl  20838  cmetcaulem  20934  ovollb2lem  21106  ovolctb  21108  ovolshftlem1  21127  ovolscalem1  21131  ovolicc1  21134  ioombl1lem1  21175  ioorf  21189  ioorcl  21193  dyadf  21207  vitalilem2  21225  vitali  21229  i1faddlem  21307  dvres2lem  21521  dvaddbr  21548  dvmulbr  21549  lhop1lem  21621  lhop  21624  dvcnvrelem2  21626  ig1peu  21779  tayl0  21963  rlimcnp2  22496  xrlimcnp  22498  ppisval  22577  ppisval2  22578  ppinprm  22626  chtnprm  22628  2sqlem7  22845  chebbnd1lem1  22854  foot  23256  perprag  23257  colperpexlem3  23261  mideulem  23263  lmieu  23276  f1otrg  23289  eengtrkg  23403  mndomgmid  24001  shuni  24875  5oalem1  25229  5oalem2  25230  5oalem4  25232  5oalem5  25233  3oalem2  25238  pjclem4  25775  pj3si  25783  xrge0tsmsd  26418  prsdm  26509  prsrn  26510  pnfneige0  26546  qqhucn  26586  gsumesum  26675  esumcst  26679  sigainb  26744  eulerpartlemgh  26925  eulerpartlemgs2  26927  eulerpartlemn  26928  sseqmw  26938  sseqf  26939  sseqp1  26942  fibp1  26948  cnllyscon  27298  rellyscon  27304  cvmsss2  27327  cvmcov2  27328  cvmopnlem  27331  blbnd  28854  ssbnd  28855  heiborlem1  28878  heiborlem8  28885  heibor  28888  elrfi  29198  elrfirn  29199  fnwe2lem2  29572  dfac11  29583  kelac1  29584  kelac2lem  29585  dfac21  29587  islssfgi  29593  filnm  29611  lpirlnr  29641  hbtlem6  29653  hbt  29654  cntzsdrg  29727  iocinico  29755  stoweidlem57  30020  pmatcoe1fsupp  31212  bnj1379  32176  bnj1177  32349  pmodlem1  33848  pclfinN  33902  mapdunirnN  35653  hdmaprnlem9N  35863