Theorem elind 4195

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

Syntax hints:   → wi 4   ∈ wcel 2107   ∩ cin 3948

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-tru 1545  df-ex 1783  df-sb 2069  df-clab 2711  df-cleq 2725  df-clel 2811  df-v 3477  df-in 3956

This theorem is referenced by:  fvelimad  6960  fnfvimad  7236  tfrlem5  8380  uniinqs  8791  unifpw  9355  f1opwfi  9356  fissuni  9357  fipreima  9358  elfir  9410  inelfi  9413  cantnfcl  9662  frrlem15  9752  tskwe  9945  infpwfidom  10023  infpwfien  10057  ackbij2lem1  10214  ackbij1lem3  10217  ackbij1lem4  10218  ackbij1lem6  10220  ackbij1lem11  10225  fin23lem24  10317  isfin1-3  10381  fpwwe2lem11  10636  fpwwe  10641  canthnumlem  10643  fz1isolem  14422  isprm7  16645  setsstruct2  17107  strfv2d  17135  submre  17549  submrc  17572  isacs2  17597  coffth  17887  catcoppccl  18067  catcoppcclOLD  18068  catcfuccl  18069  catcfucclOLD  18070  catcxpccl  18159  catcxpcclOLD  18160  isdrs2  18259  fpwipodrs  18493  insubm  18699  sylow2a  19487  lsmmod  19543  lsmdisj  19549  lsmdisj2  19550  subgdisj1  19559  frgpnabllem1  19741  dmdprdd  19869  dprdfeq0  19892  dprdres  19898  dprddisj2  19909  dprd2da  19912  dmdprdsplit2lem  19915  ablfacrp  19936  pgpfac1lem3a  19946  pgpfac1lem3  19947  pgpfaclem1  19951  cntzsdrg  20418  2idl0  20863  2idl1  20864  zringlpirlem1  21032  zringlpirlem3  21034  aspval  21427  mplind  21631  pmatcoe1fsupp  22203  baspartn  22457  bastg  22469  clsval2  22554  isopn3  22570  restbas  22662  lmss  22802  cmpcovf  22895  discmp  22902  cmpsublem  22903  cmpsub  22904  isconn2  22918  connclo  22919  llynlly  22981  restnlly  22986  restlly  22987  islly2  22988  llyrest  22989  nllyrest  22990  llyidm  22992  nllyidm  22993  hausllycmp  22998  cldllycmp  22999  lly1stc  23000  dislly  23001  llycmpkgen2  23054  1stckgenlem  23057  txlly  23140  txnlly  23141  txtube  23144  txcmplem1  23145  txcmplem2  23146  xkococnlem  23163  basqtop  23215  tgqtop  23216  infil  23367  fmfnfmlem4  23461  hauspwpwf1  23491  tgpconncompss  23618  ustfilxp  23717  metrest  24033  tgioo  24312  zdis  24332  icccmplem1  24338  icccmplem2  24339  reconnlem2  24343  xrge0tsms  24350  cnheibor  24471  cnllycmp  24472  ncvs1  24674  cphsqrtcl  24701  cmetcaulem  24805  ovollb2lem  25005  ovolctb  25007  ovolshftlem1  25026  ovolscalem1  25030  ovolicc1  25033  ioombl1lem1  25075  ioorf  25090  ioorcl  25094  dyadf  25108  vitalilem2  25126  vitali  25130  i1faddlem  25210  i1fmullem  25211  dvres2lem  25427  dvaddbr  25455  dvmulbr  25456  lhop1lem  25530  lhop  25533  dvcnvrelem2  25535  ig1peu  25689  tayl0  25874  rlimcnp2  26471  xrlimcnp  26473  ppisval  26608  ppisval2  26609  ppinprm  26656  chtnprm  26658  2sqlem7  26927  chebbnd1lem1  26972  footexALT  27969  footexlem2  27971  foot  27973  footne  27974  perprag  27977  colperpexlem3  27983  mideulem2  27985  lnopp2hpgb  28014  colopp  28020  lmieu  28035  lmimid  28045  hypcgrlem1  28050  hypcgrlem2  28051  trgcopyeulem  28056  f1otrg  28122  eengtrkg  28244  shuni  30553  5oalem1  30907  5oalem2  30908  5oalem4  30910  5oalem5  30911  3oalem2  30916  pjclem4  31452  pj3si  31460  ccatf1  32115  xrge0tsmsd  32209  idlinsubrg  32549  qsdrngilem  32608  qsdrngi  32609  lindsunlem  32709  lbsdiflsp0  32711  dimkerim  32712  irngss  32751  cmpcref  32830  cmppcmp  32838  dispcmp  32839  zarcmplem  32861  prsdm  32894  prsrn  32895  pnfneige0  32931  qqhucn  32972  rrhqima  32994  gsumesum  33057  esumcst  33061  esum2d  33091  sigainb  33134  inelpisys  33152  dynkin  33165  eulerpartlemgh  33377  eulerpartlemgs2  33379  eulerpartlemn  33380  sseqmw  33390  sseqf  33391  sseqp1  33394  fibp1  33400  bnj1379  33841  bnj1177  34017  cnllysconn  34236  rellysconn  34242  cvmsss2  34265  cvmcov2  34266  cvmopnlem  34269  mclsind  34561  gg-dvmulbr  35175  poimirlem30  36518  blbnd  36655  ssbnd  36656  heiborlem1  36679  heiborlem8  36686  heibor  36689  mndomgmid  36739  pmodlem1  38717  pclfinN  38771  mapdunirnN  40521  hdmaprnlem9N  40728  mhpind  41166  elrfi  41432  elrfirn  41433  fnwe2lem2  41793  dfac11  41804  kelac1  41805  kelac2lem  41806  dfac21  41808  islssfgi  41814  filnm  41832  lpirlnr  41859  hbtlem6  41871  hbt  41872  iocinico  41961  restuni3  43807  disjinfi  43891  fvelima2  43964  iooabslt  44212  iocopn  44233  icoopn  44238  uzinico  44273  limciccioolb  44337  limcicciooub  44353  islpcn  44355  limcresioolb  44359  limcleqr  44360  limsuppnfdlem  44417  limsupresxr  44482  liminfresxr  44483  liminfvalxr  44499  liminflelimsupuz  44501  cnrefiisplem  44545  ioccncflimc  44601  icccncfext  44603  icocncflimc  44605  cncfiooicclem1  44609  itgiccshift  44696  itgperiod  44697  itgsbtaddcnst  44698  stoweidlem57  44773  fourierdlem20  44843  fourierdlem32  44855  fourierdlem33  44856  fourierdlem48  44870  fourierdlem49  44871  fourierdlem62  44884  fourierdlem71  44893  fouriersw  44947  qndenserrnbllem  45010  qndenserrn  45015  salgencntex  45059  fsumlesge0  45093  sge0tsms  45096  sge0cl  45097  sge0f1o  45098  sge0sup  45107  sge0resplit  45122  sge0iunmptlemre  45131  sge0fodjrnlem  45132  sge0rpcpnf  45137  sge0xaddlem1  45149  ovolval4lem2  45366  sssmf  45454  smflimlem3  45489  smfsuplem1  45527  fcores  45777  prproropf1olem2  46172  zrinitorngc  46898  zrtermorngc  46899  zrzeroorngc  46900  irinitoringc  46967  zrtermoringc  46968  zrninitoringc  46969  nzerooringczr  46970  thincciso  47669