Theorem elind 4140

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

Syntax hints:   → wi 4   ∈ wcel 2114   ∩ cin 3888

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2715  df-cleq 2728  df-clel 2811  df-v 3431  df-in 3896

This theorem is referenced by:  fvelima2  6892  fvelimad  6907  fnfvimad  7189  tfrlem5  8319  uniinqs  8744  unifpw  9265  f1opwfi  9266  fissuni  9267  fipreima  9268  elfir  9328  inelfi  9331  cantnfcl  9588  frrlem15  9681  tskwe  9874  infpwfidom  9950  infpwfien  9984  ackbij2lem1  10140  ackbij1lem3  10143  ackbij1lem4  10144  ackbij1lem6  10146  ackbij1lem11  10151  fin23lem24  10244  isfin1-3  10308  fpwwe2lem11  10564  fpwwe  10569  canthnumlem  10571  fz1isolem  14423  isprm7  16678  setsstruct2  17144  strfv2d  17171  submre  17567  submrc  17594  isacs2  17619  coffth  17905  catcoppccl  18084  catcfuccl  18085  catcxpccl  18173  isdrs2  18272  fpwipodrs  18506  insubm  18786  sylow2a  19594  lsmmod  19650  lsmdisj  19656  lsmdisj2  19657  subgdisj1  19666  frgpnabllem1  19848  dmdprdd  19976  dprdfeq0  19999  dprdres  20005  dprddisj2  20016  dprd2da  20019  dmdprdsplit2lem  20022  ablfacrp  20043  pgpfac1lem3a  20053  pgpfac1lem3  20054  pgpfaclem1  20058  zrinitorngc  20619  zrtermorngc  20620  zrzeroorngc  20621  zrtermoringc  20652  zrninitoringc  20653  cntzsdrg  20779  2idl0  21258  2idl1  21259  zringlpirlem1  21442  zringlpirlem3  21444  irinitoringc  21459  nzerooringczr  21460  aspval  21852  mplind  22048  pmatcoe1fsupp  22666  baspartn  22919  bastg  22931  clsval2  23015  isopn3  23031  restbas  23123  lmss  23263  cmpcovf  23356  discmp  23363  cmpsublem  23364  cmpsub  23365  isconn2  23379  connclo  23380  llynlly  23442  restnlly  23447  restlly  23448  islly2  23449  llyrest  23450  nllyrest  23451  llyidm  23453  nllyidm  23454  hausllycmp  23459  cldllycmp  23460  lly1stc  23461  dislly  23462  llycmpkgen2  23515  1stckgenlem  23518  txlly  23601  txnlly  23602  txtube  23605  txcmplem1  23606  txcmplem2  23607  xkococnlem  23624  basqtop  23676  tgqtop  23677  infil  23828  fmfnfmlem4  23922  hauspwpwf1  23952  tgpconncompss  24079  ustfilxp  24178  metrest  24489  tgioo  24761  zdis  24782  icccmplem1  24788  icccmplem2  24789  reconnlem2  24793  xrge0tsms  24800  cnheibor  24922  cnllycmp  24923  ncvs1  25124  cphsqrtcl  25151  cmetcaulem  25255  ovollb2lem  25455  ovolctb  25457  ovolshftlem1  25476  ovolscalem1  25480  ovolicc1  25483  ioombl1lem1  25525  ioorf  25540  ioorcl  25544  dyadf  25558  vitalilem2  25576  vitali  25580  i1faddlem  25660  i1fmullem  25661  dvres2lem  25877  dvaddbr  25905  dvmulbr  25906  lhop1lem  25980  lhop  25983  dvcnvrelem2  25985  ig1peu  26140  tayl0  26327  rlimcnp2  26930  xrlimcnp  26932  ppisval  27067  ppisval2  27068  ppinprm  27115  chtnprm  27117  2sqlem7  27387  chebbnd1lem1  27432  footexALT  28786  footexlem2  28788  foot  28790  footne  28791  perprag  28794  colperpexlem3  28800  mideulem2  28802  lnopp2hpgb  28831  colopp  28837  lmieu  28852  lmimid  28862  hypcgrlem1  28867  hypcgrlem2  28868  trgcopyeulem  28873  f1otrg  28939  eengtrkg  29055  shuni  31371  5oalem1  31725  5oalem2  31726  5oalem4  31728  5oalem5  31729  3oalem2  31734  pjclem4  32270  pj3si  32278  ccatf1  33009  xrge0tsmsd  33134  wrdpmtrlast  33154  idlinsubrg  33491  ssdifidlprm  33518  qsdrngilem  33554  qsdrngi  33555  pidufd  33603  exsslsb  33741  lindsunlem  33768  lbsdiflsp0  33770  dimkerim  33771  irngss  33831  cmpcref  33994  cmppcmp  34002  dispcmp  34003  zarcmplem  34025  prsdm  34058  prsrn  34059  pnfneige0  34095  qqhucn  34136  rrhqima  34158  gsumesum  34203  esumcst  34207  esum2d  34237  sigainb  34280  inelpisys  34298  dynkin  34311  eulerpartlemgh  34522  eulerpartlemgs2  34524  eulerpartlemn  34525  sseqmw  34535  sseqf  34536  sseqp1  34539  fibp1  34545  bnj1379  34972  bnj1177  35148  cnllysconn  35427  rellysconn  35433  cvmsss2  35456  cvmcov2  35457  cvmopnlem  35460  mclsind  35752  weiunfr  36649  poimirlem30  37971  blbnd  38108  ssbnd  38109  heiborlem1  38132  heiborlem8  38139  heibor  38142  mndomgmid  38192  pmodlem1  40292  pclfinN  40346  mapdunirnN  42096  hdmaprnlem9N  42303  mhpind  43027  elrfi  43126  elrfirn  43127  fnwe2lem2  43479  dfac11  43490  kelac1  43491  kelac2lem  43492  dfac21  43494  islssfgi  43500  filnm  43518  lpirlnr  43545  hbtlem6  43557  hbt  43558  iocinico  43640  restuni3  45548  disjinfi  45622  iooabslt  45929  iocopn  45950  icoopn  45955  uzinico  45989  limciccioolb  46051  limcicciooub  46065  islpcn  46067  limcresioolb  46071  limcleqr  46072  limsuppnfdlem  46129  limsupresxr  46194  liminfresxr  46195  liminfvalxr  46211  liminflelimsupuz  46213  cnrefiisplem  46257  ioccncflimc  46313  icccncfext  46315  icocncflimc  46317  cncfiooicclem1  46321  itgiccshift  46408  itgperiod  46409  itgsbtaddcnst  46410  stoweidlem57  46485  fourierdlem20  46555  fourierdlem32  46567  fourierdlem33  46568  fourierdlem48  46582  fourierdlem49  46583  fourierdlem62  46596  fourierdlem71  46605  fouriersw  46659  qndenserrnbllem  46722  qndenserrn  46727  salgencntex  46771  fsumlesge0  46805  sge0tsms  46808  sge0cl  46809  sge0f1o  46810  sge0sup  46819  sge0resplit  46834  sge0iunmptlemre  46843  sge0fodjrnlem  46844  sge0rpcpnf  46849  sge0xaddlem1  46861  ovolval4lem2  47078  sssmf  47166  smflimlem3  47201  smfsuplem1  47239  fcores  47515  prproropf1olem2  47964  iinfconstbaslem  49540  ffthoppf  49640  uobeqw  49694  uobeq  49695  swapfiso  49760  swapciso  49761  fucoppcffth  49886  thincciso  49928  thinccisod  49929  termcterm  49988  termcterm2  49989  termcterm3  49990  termcciso  49991  termc2  49993  diagciso  50014  diagcic  50015  uobeqterm  50021