Theorem elind 4153

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2146   ∩ cin 3905

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 2148  ax-9 2156  ax-ext 2737

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2744  df-cleq 2757  df-clel 2840  df-v 3459  df-in 3913

This theorem is used by:  fvelima2  6937  fvelimad  6952  fnfvimad  7239  tfrlem5  8372  uniinqs  8801  unifpw  9319  f1opwfi  9320  fissuni  9321  fipreima  9322  elfir  9382  inelfi  9385  cantnfcl  9643  frrlem15  9736  tskwe  9952  infpwfidom  10028  infpwfien  10062  ackbij2lem1  10217  ackbij1lem3  10220  ackbij1lem4  10221  ackbij1lem6  10223  ackbij1lem11  10228  fin23lem24  10321  isfin1-3  10385  fpwwe2lem11  10641  fpwwe  10646  canthnumlem  10648  fz1isolem  14516  ccatf1  14646  isprm7  16789  setsstruct2  17256  strfv2d  17283  submre  17679  submrc  17706  isacs2  17731  coffth  18017  catcoppccl  18196  catcfuccl  18197  catcxpccl  18285  isdrs2  18384  fpwipodrs  18618  insubm  18914  sylow2a  19733  lsmmod  19789  lsmdisj  19795  lsmdisj2  19796  subgdisj1  19805  frgpnabllem1  19987  dmdprdd  20115  dprdfeq0  20138  dprdres  20144  dprddisj2  20155  dprd2da  20158  dmdprdsplit2lem  20161  ablfacrp  20182  pgpfac1lem3a  20192  pgpfac1lem3  20193  pgpfaclem1  20197  zrinitorngc  20791  zrtermorngc  20792  zrzeroorngc  20793  zrtermoringc  20824  zrninitoringc  20825  cntzsdrg  20955  2idl0  21449  2idl1  21450  ssdifidlprm  21536  zringlpirlem1  21662  zringlpirlem3  21664  irinitoringc  21679  nzerooringczr  21680  aspval  22072  mplind  22271  pmatcoe1fsupp  22908  baspartn  23161  bastg  23173  clsval2  23257  isopn3  23273  restbas  23365  lmss  23505  cmpcovf  23598  discmp  23605  cmpsublem  23606  cmpsub  23607  isconn2  23621  connclo  23622  llynlly  23685  restnlly  23690  restlly  23691  islly2  23692  llyrest  23693  nllyrest  23694  llyidm  23696  nllyidm  23697  hausllycmp  23702  cldllycmp  23703  lly1stc  23704  dislly  23705  llycmpkgen2  23758  1stckgenlem  23761  txlly  23844  txnlly  23845  txtube  23848  txcmplem1  23849  txcmplem2  23850  xkococnlem  23867  basqtop  23919  tgqtop  23920  infil  24071  fmfnfmlem4  24165  hauspwpwf1  24195  tgpconncompss  24322  ustfilxp  24421  metrest  24732  tgioo  25004  zdis  25025  icccmplem1  25031  icccmplem2  25032  reconnlem2  25036  xrge0tsms  25043  cnheibor  25165  cnllycmp  25166  ncvs1  25367  cphsqrtcl  25394  cmetcaulem  25498  ovollb2lem  25698  ovolctb  25700  ovolshftlem1  25719  ovolscalem1  25723  ovolicc1  25726  ioombl1lem1  25768  ioorf  25783  ioorcl  25787  dyadf  25801  vitalilem2  25819  vitali  25823  i1faddlem  25903  i1fmullem  25904  dvres2lem  26120  dvaddbr  26148  dvmulbr  26149  lhop1lem  26223  lhop  26226  dvcnvrelem2  26228  ig1peu  26383  tayl0  26576  rlimcnp2  27182  xrlimcnp  27184  ppisval  27319  ppisval2  27320  ppinprm  27367  chtnprm  27369  2sqlem7  27639  chebbnd1lem1  27684  tglnpt4  28979  footexALT  29049  footexlem2  29051  foot  29053  footne  29054  perprag  29058  colperpexlem3  29064  mideulem2  29066  lnopp2hpgb  29096  colopp  29102  lnincplng  29117  plngrotlem1  29120  plngrotlem2  29121  lnssplng  29125  lmieu  29144  lmimid  29154  hypcgrlem1  29160  hypcgrlem2  29161  trgcopyeulem  29167  tgaaddcpbllem1  29203  tgaaddcpbl  29206  dfprlng2  29252  prlngmolem1  29257  prlngmolem2  29258  prlngmo2  29261  prlngpln4  29263  prlngmid2  29266  prlngsymquadlem  29268  quadcgrprlng  29271  f1otrg  29275  eengtrkg  29391  shuni  31723  5oalem1  32077  5oalem2  32078  5oalem4  32080  5oalem5  32081  3oalem2  32086  pjclem4  32622  pj3si  32630  xrge0tsmsd  33457  wrdpmtrlast  33477  idlinsubrg  33803  qsdrngilem  33840  qsdrngi  33841  pidufd  33897  exsslsb  34051  lindsunlem  34078  lbsdiflsp0  34080  dimkerim  34081  irngss  34141  cmpcref  34304  cmppcmp  34312  dispcmp  34313  zarcmplem  34335  prsdm  34368  prsrn  34369  pnfneige0  34405  qqhucn  34446  rrhqima  34468  gsumesum  34513  esumcst  34517  esum2d  34547  sigainb  34591  inelpisys  34609  dynkin  34622  eulerpartlemgh  34833  eulerpartlemgs2  34835  eulerpartlemn  34836  sseqmw  34846  sseqf  34847  sseqp1  34850  fibp1  34856  bnj1379  35283  bnj1177  35459  cnllysconn  35774  rellysconn  35780  cvmsss2  35803  cvmcov2  35804  cvmopnlem  35807  mclsind  36099  weiunfr  37035  poimirlem30  38358  blbnd  38496  ssbnd  38497  heiborlem1  38520  heiborlem8  38527  heibor  38530  mndomgmid  38580  pmodlem1  40678  pclfinN  40732  mapdunirnN  42482  hdmaprnlem9N  42689  mhpind  43384  elrfi  43483  elrfirn  43484  fnwe2lem2  43836  dfac11  43847  kelac1  43848  kelac2lem  43849  dfac21  43851  islssfgi  43857  filnm  43875  lpirlnr  43902  hbtlem6  43914  hbt  43915  iocinico  43997  restuni3  45894  disjinfi  45968  iooabslt  46273  iocopn  46294  icoopn  46299  uzinico  46333  limciccioolb  46395  limcicciooub  46409  islpcn  46411  limcresioolb  46415  limcleqr  46416  limsuppnfdlem  46473  limsupresxr  46538  liminfresxr  46539  liminfvalxr  46555  liminflelimsupuz  46557  cnrefiisplem  46601  ioccncflimc  46657  icccncfext  46659  icocncflimc  46661  cncfiooicclem1  46665  itgiccshift  46752  itgperiod  46753  itgsbtaddcnst  46754  stoweidlem57  46829  fourierdlem20  46899  fourierdlem32  46911  fourierdlem33  46912  fourierdlem48  46926  fourierdlem49  46927  fourierdlem62  46940  fourierdlem71  46949  fouriersw  47003  qndenserrnbllem  47066  qndenserrn  47071  salgencntex  47115  fsumlesge0  47149  sge0tsms  47152  sge0cl  47153  sge0f1o  47154  sge0sup  47163  sge0resplit  47178  sge0iunmptlemre  47187  sge0fodjrnlem  47188  sge0rpcpnf  47193  sge0xaddlem1  47205  ovolval4lem2  47422  sssmf  47510  smflimlem3  47545  smfsuplem1  47583  fcores  47862  prproropf1olem2  48311  iinfconstbaslem  49900  ffthoppf  50000  uobeqw  50054  uobeq  50055  swapfiso  50120  swapciso  50121  fucoppcffth  50246  thincciso  50288  thinccisod  50289  termcterm  50348  termcterm2  50349  termcterm3  50350  termcciso  50351  termc2  50353  diagciso  50374  diagcic  50375  uobeqterm  50381