Theorem elind 4096

Description: Deduce membership in an intersection of two classes. (Contributed by Jonathan Ben-Naim, 3-Jun-2011.)

Hypotheses

Ref	Expression
elind.1	⊢ (𝜑 → 𝑋 ∈ 𝐴)
elind.2	⊢ (𝜑 → 𝑋 ∈ 𝐵)

Assertion

Ref	Expression
elind	⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

Proof of Theorem elind

Step	Hyp	Ref	Expression
1		elind.1	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐴)
2		elind.2	. 2 ⊢ (𝜑 → 𝑋 ∈ 𝐵)
3		elin 4092	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2144   ∩ cin 4088

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1827  ax-4 1841  ax-5 1942  ax-6 1999  ax-7 2040  ax-8 2146  ax-9 2154  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1572  df-ex 1812  df-sb 2099  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 4090

This theorem is used by:  fvelima2  6940  fvelimad  6955  fnfvimad  7242  fnwe2lem3  8151  tfrlem5  8392  uniinqs  8823  unifpw  9349  f1opwfi  9350  fissuni  9351  fipreima  9352  elfir  9412  inelfi  9415  cantnfcl  9673  frrlem15  9766  tskwe  10036  infpwfidom  10112  infpwfien  10146  ackbij2lem1  10301  ackbij1lem3  10304  ackbij1lem4  10305  ackbij1lem6  10307  ackbij1lem11  10312  fin23lem24  10405  isfin1-3  10469  fpwwe2lem11  10731  fpwwe  10736  canthnumlem  10738  fz1isolem  14611  ccatf1  14741  isprm7  16891  setsstruct2  17359  strfv2d  17386  submre  17782  submrc  17809  isacs2  17834  coffth  18120  catcoppccl  18299  catcfuccl  18300  catcxpccl  18388  isdrs2  18487  fpwipodrs  18721  insubm  19021  sylow2a  19840  lsmmod  19896  lsmdisj  19902  lsmdisj2  19903  subgdisj1  19912  frgpnabllem1  20094  dmdprdd  20222  dprdfeq0  20245  dprdres  20251  dprddisj2  20262  dprd2da  20265  dmdprdsplit2lem  20268  ablfacrp  20289  pgpfac1lem3a  20299  pgpfac1lem3  20300  pgpfaclem1  20304  zrinitorngc  20901  zrtermorngc  20902  zrzeroorngc  20903  zrtermoringc  20934  zrninitoringc  20935  cntzsdrg  21066  2idl0  21561  2idl1  21562  ssdifidlprm  21649  zringlpirlem1  21775  zringlpirlem3  21777  irinitoringc  21792  nzerooringczr  21793  aspval  22187  mplind  22386  pmatcoe1fsupp  23026  baspartn  23279  bastg  23291  clsval2  23375  isopn3  23391  restbas  23483  lmss  23623  cmpcovf  23716  discmp  23723  cmpsublem  23724  cmpsub  23725  isconn2  23739  connclo  23740  llynlly  23803  restnlly  23808  restlly  23809  islly2  23810  llyrest  23811  nllyrest  23812  llyidm  23814  nllyidm  23815  hausllycmp  23820  cldllycmp  23821  lly1stc  23822  dislly  23823  llycmpkgen2  23876  1stckgenlem  23879  txlly  23962  txnlly  23963  txtube  23966  txcmplem1  23967  txcmplem2  23968  xkococnlem  23985  basqtop  24037  tgqtop  24038  infil  24189  fmfnfmlem4  24283  hauspwpwf1  24313  tgpconncompss  24440  ustfilxp  24539  metrest  24850  tgioo  25122  zdis  25143  icccmplem1  25149  icccmplem2  25150  reconnlem2  25154  xrge0tsms  25161  cnheibor  25283  cnllycmp  25284  ncvs1  25485  cphsqrtcl  25512  cmetcaulem  25616  ovollb2lem  25816  ovolctb  25818  ovolshftlem1  25837  ovolscalem1  25841  ovolicc1  25844  ioombl1lem1  25886  ioorf  25901  ioorcl  25905  dyadf  25919  vitalilem2  25937  vitali  25941  i1faddlem  26021  i1fmullem  26022  dvres2lem  26237  dvaddbr  26265  dvmulbr  26266  lhop1lem  26340  lhop  26343  dvcnvrelem2  26345  ig1peu  26500  tayl0  26696  rlimcnp2  27301  xrlimcnp  27303  ppisval  27438  ppisval2  27439  ppinprm  27486  chtnprm  27488  2sqlem7  27758  chebbnd1lem1  27803  tglnpt4  29130  footexALT  29200  footexlem2  29202  foot  29204  footne  29205  perprag  29209  colperpexlem3  29215  mideulem2  29217  lnoppinn0  29238  lnopp2hpgb  29248  colopp  29254  lnincplng  29269  plngrotlem1  29272  plngrotlem2  29273  lnssplng  29277  lmieu  29296  lmimid  29306  hypcgrlem1  29312  hypcgrlem2  29313  trgcopyeulem  29319  tgaaddcpbllem1  29356  tgaaddcpbl  29359  angmgmaddeu2  29387  angmgmaddeu3  29388  angmgmaddov2lem  29394  angmgmaddcpbl  29397  angmgmaddrid  29400  dfprlng2  29432  prlngmolem1  29437  prlngmolem2  29438  prlngmo2  29441  prlngpln4  29443  prlngmid2  29446  prlngsymquadlem  29448  quadcgrprlng  29451  f1otrg  29455  eengtrkg  29571  shuni  31909  5oalem1  32263  5oalem2  32264  5oalem4  32266  5oalem5  32267  3oalem2  32272  pjclem4  32808  pj3si  32816  xrge0tsmsd  33682  wrdpmtrlast  33702  idlinsubrg  34029  qsdrngilem  34066  qsdrngi  34067  pidufd  34123  exsslsb  34277  lindsunlem  34304  lbsdiflsp0  34306  dimkerim  34307  irngss  34367  cmpcref  34530  cmppcmp  34538  dispcmp  34539  zarcmplem  34561  prsdm  34594  prsrn  34595  pnfneige0  34631  qqhucn  34672  rrhqima  34694  gsumesum  34739  esumcst  34743  esum2d  34773  sigainb  34817  inelpisys  34835  dynkin  34848  eulerpartlemgh  35058  eulerpartlemgs2  35060  eulerpartlemn  35061  sseqmw  35071  sseqf  35072  sseqp1  35075  fibp1  35081  bnj1379  35508  bnj1177  35684  cnllysconn  36098  rellysconn  36104  cvmsss2  36127  cvmcov2  36128  cvmopnlem  36131  mclsind  36423  weiunfr  37349  poimirlem30  38675  blbnd  38828  ssbnd  38829  heiborlem1  38852  heiborlem8  38859  heibor  38862  mndomgmid  38912  pmodlem1  41010  pclfinN  41064  mapdunirnN  42814  hdmaprnlem9N  43021  mhpind  43729  elrfi  43812  elrfirn  43813  dfac11  44171  kelac1  44172  kelac2lem  44173  dfac21  44175  islssfgi  44181  filnm  44199  lpirlnr  44226  hbtlem6  44238  hbt  44239  iocinico  44321  ishfstruct  46135  restuni3  46240  disjinfi  46314  iooabslt  46618  iocopn  46639  icoopn  46644  uzinico  46678  limciccioolb  46740  limcicciooub  46754  islpcn  46756  limcresioolb  46760  limcleqr  46761  limsuppnfdlem  46818  limsupresxr  46883  liminfresxr  46884  liminfvalxr  46900  liminflelimsupuz  46902  cnrefiisplem  46946  ioccncflimc  47002  icccncfext  47004  icocncflimc  47006  cncfiooicclem1  47010  itgiccshift  47097  itgperiod  47098  itgsbtaddcnst  47099  stoweidlem57  47174  fourierdlem20  47244  fourierdlem32  47256  fourierdlem33  47257  fourierdlem48  47271  fourierdlem49  47272  fourierdlem62  47285  fourierdlem71  47294  fouriersw  47348  qndenserrnbllem  47411  qndenserrn  47416  salgencntex  47460  fsumlesge0  47494  sge0tsms  47497  sge0cl  47498  sge0f1o  47499  sge0sup  47508  sge0resplit  47523  sge0iunmptlemre  47532  sge0fodjrnlem  47533  sge0rpcpnf  47538  sge0xaddlem1  47550  ovolval4lem2  47767  sssmf  47855  smflimlem3  47890  smfsuplem1  47928  fcores  48244  prproropf1olem2  48693  iinfconstbaslem  50286  ffthoppf  50388  uobeqw  50442  uobeq  50443  swapfiso  50514  swapciso  50515  fucoppcffth  50653  thincciso  50695  thinccisod  50696  termcterm  50755  termcterm2  50756  termcterm3  50757  termcciso  50758  termc2  50760  diagciso  50784  diagcic  50785  uobeqterm  50791