Theorem elind 4146

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 3915	. 2 ⊢ (𝑋 ∈ (𝐴 ∩ 𝐵) ↔ (𝑋 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵))
4	1, 2, 3	sylanbrc 595	1 ⊢ (𝜑 → 𝑋 ∈ (𝐴 ∩ 𝐵))

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2733

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3453  df-in 3906

This theorem is used by:  fvelima2  6935  fvelimad  6950  fnfvimad  7238  tfrlem5  8380  uniinqs  8811  unifpw  9337  f1opwfi  9338  fissuni  9339  fipreima  9340  elfir  9400  inelfi  9403  cantnfcl  9661  frrlem15  9754  tskwe  10024  infpwfidom  10100  infpwfien  10134  ackbij2lem1  10289  ackbij1lem3  10292  ackbij1lem4  10293  ackbij1lem6  10295  ackbij1lem11  10300  fin23lem24  10393  isfin1-3  10457  fpwwe2lem11  10719  fpwwe  10724  canthnumlem  10726  fz1isolem  14599  ccatf1  14729  isprm7  16877  setsstruct2  17345  strfv2d  17372  submre  17768  submrc  17795  isacs2  17820  coffth  18106  catcoppccl  18285  catcfuccl  18286  catcxpccl  18374  isdrs2  18473  fpwipodrs  18707  insubm  19007  sylow2a  19826  lsmmod  19882  lsmdisj  19888  lsmdisj2  19889  subgdisj1  19898  frgpnabllem1  20080  dmdprdd  20208  dprdfeq0  20231  dprdres  20237  dprddisj2  20248  dprd2da  20251  dmdprdsplit2lem  20254  ablfacrp  20275  pgpfac1lem3a  20285  pgpfac1lem3  20286  pgpfaclem1  20290  zrinitorngc  20887  zrtermorngc  20888  zrzeroorngc  20889  zrtermoringc  20920  zrninitoringc  20921  cntzsdrg  21052  2idl0  21547  2idl1  21548  ssdifidlprm  21635  zringlpirlem1  21761  zringlpirlem3  21763  irinitoringc  21778  nzerooringczr  21779  aspval  22173  mplind  22372  pmatcoe1fsupp  23012  baspartn  23265  bastg  23277  clsval2  23361  isopn3  23377  restbas  23469  lmss  23609  cmpcovf  23702  discmp  23709  cmpsublem  23710  cmpsub  23711  isconn2  23725  connclo  23726  llynlly  23789  restnlly  23794  restlly  23795  islly2  23796  llyrest  23797  nllyrest  23798  llyidm  23800  nllyidm  23801  hausllycmp  23806  cldllycmp  23807  lly1stc  23808  dislly  23809  llycmpkgen2  23862  1stckgenlem  23865  txlly  23948  txnlly  23949  txtube  23952  txcmplem1  23953  txcmplem2  23954  xkococnlem  23971  basqtop  24023  tgqtop  24024  infil  24175  fmfnfmlem4  24269  hauspwpwf1  24299  tgpconncompss  24426  ustfilxp  24525  metrest  24836  tgioo  25108  zdis  25129  icccmplem1  25135  icccmplem2  25136  reconnlem2  25140  xrge0tsms  25147  cnheibor  25269  cnllycmp  25270  ncvs1  25471  cphsqrtcl  25498  cmetcaulem  25602  ovollb2lem  25802  ovolctb  25804  ovolshftlem1  25823  ovolscalem1  25827  ovolicc1  25830  ioombl1lem1  25872  ioorf  25887  ioorcl  25891  dyadf  25905  vitalilem2  25923  vitali  25927  i1faddlem  26007  i1fmullem  26008  dvres2lem  26223  dvaddbr  26251  dvmulbr  26252  lhop1lem  26326  lhop  26329  dvcnvrelem2  26331  ig1peu  26486  tayl0  26682  rlimcnp2  27287  xrlimcnp  27289  ppisval  27424  ppisval2  27425  ppinprm  27472  chtnprm  27474  2sqlem7  27744  chebbnd1lem1  27789  tglnpt4  29116  footexALT  29186  footexlem2  29188  foot  29190  footne  29191  perprag  29195  colperpexlem3  29201  mideulem2  29203  lnoppinn0  29224  lnopp2hpgb  29234  colopp  29240  lnincplng  29255  plngrotlem1  29258  plngrotlem2  29259  lnssplng  29263  lmieu  29282  lmimid  29292  hypcgrlem1  29298  hypcgrlem2  29299  trgcopyeulem  29305  tgaaddcpbllem1  29342  tgaaddcpbl  29345  angmgmaddeu2  29373  angmgmaddeu3  29374  angmgmaddov2lem  29380  angmgmaddcpbl  29383  angmgmaddrid  29386  dfprlng2  29418  prlngmolem1  29423  prlngmolem2  29424  prlngmo2  29427  prlngpln4  29429  prlngmid2  29432  prlngsymquadlem  29434  quadcgrprlng  29437  f1otrg  29441  eengtrkg  29557  shuni  31895  5oalem1  32249  5oalem2  32250  5oalem4  32252  5oalem5  32253  3oalem2  32258  pjclem4  32794  pj3si  32802  xrge0tsmsd  33627  wrdpmtrlast  33647  idlinsubrg  33974  qsdrngilem  34011  qsdrngi  34012  pidufd  34068  exsslsb  34222  lindsunlem  34249  lbsdiflsp0  34251  dimkerim  34252  irngss  34312  cmpcref  34475  cmppcmp  34483  dispcmp  34484  zarcmplem  34506  prsdm  34539  prsrn  34540  pnfneige0  34576  qqhucn  34617  rrhqima  34639  gsumesum  34684  esumcst  34688  esum2d  34718  sigainb  34762  inelpisys  34780  dynkin  34793  eulerpartlemgh  35003  eulerpartlemgs2  35005  eulerpartlemn  35006  sseqmw  35016  sseqf  35017  sseqp1  35020  fibp1  35026  bnj1379  35453  bnj1177  35629  cnllysconn  35989  rellysconn  35995  cvmsss2  36018  cvmcov2  36019  cvmopnlem  36022  mclsind  36314  weiunfr  37235  poimirlem30  38548  blbnd  38701  ssbnd  38702  heiborlem1  38725  heiborlem8  38732  heibor  38735  mndomgmid  38785  pmodlem1  40883  pclfinN  40937  mapdunirnN  42687  hdmaprnlem9N  42894  mhpind  43602  elrfi  43684  elrfirn  43685  fnwe2lem2  44037  dfac11  44048  kelac1  44049  kelac2lem  44050  dfac21  44052  islssfgi  44058  filnm  44076  lpirlnr  44103  hbtlem6  44115  hbt  44116  iocinico  44198  restuni3  46102  disjinfi  46176  iooabslt  46480  iocopn  46501  icoopn  46506  uzinico  46540  limciccioolb  46602  limcicciooub  46616  islpcn  46618  limcresioolb  46622  limcleqr  46623  limsuppnfdlem  46680  limsupresxr  46745  liminfresxr  46746  liminfvalxr  46762  liminflelimsupuz  46764  cnrefiisplem  46808  ioccncflimc  46864  icccncfext  46866  icocncflimc  46868  cncfiooicclem1  46872  itgiccshift  46959  itgperiod  46960  itgsbtaddcnst  46961  stoweidlem57  47036  fourierdlem20  47106  fourierdlem32  47118  fourierdlem33  47119  fourierdlem48  47133  fourierdlem49  47134  fourierdlem62  47147  fourierdlem71  47156  fouriersw  47210  qndenserrnbllem  47273  qndenserrn  47278  salgencntex  47322  fsumlesge0  47356  sge0tsms  47359  sge0cl  47360  sge0f1o  47361  sge0sup  47370  sge0resplit  47385  sge0iunmptlemre  47394  sge0fodjrnlem  47395  sge0rpcpnf  47400  sge0xaddlem1  47412  ovolval4lem2  47629  sssmf  47717  smflimlem3  47752  smfsuplem1  47790  fcores  48106  prproropf1olem2  48555  iinfconstbaslem  50142  ffthoppf  50242  uobeqw  50296  uobeq  50297  swapfiso  50362  swapciso  50363  fucoppcffth  50488  thincciso  50530  thinccisod  50531  termcterm  50590  termcterm2  50591  termcterm3  50592  termcciso  50593  termc2  50595  diagciso  50616  diagcic  50617  uobeqterm  50623