Theorem elind 4141

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

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

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 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3432  df-in 3897

This theorem is referenced by:  fvelima2  6886  fvelimad  6901  fnfvimad  7182  tfrlem5  8312  uniinqs  8737  unifpw  9258  f1opwfi  9259  fissuni  9260  fipreima  9261  elfir  9321  inelfi  9324  cantnfcl  9579  frrlem15  9672  tskwe  9865  infpwfidom  9941  infpwfien  9975  ackbij2lem1  10131  ackbij1lem3  10134  ackbij1lem4  10135  ackbij1lem6  10137  ackbij1lem11  10142  fin23lem24  10235  isfin1-3  10299  fpwwe2lem11  10555  fpwwe  10560  canthnumlem  10562  fz1isolem  14414  isprm7  16669  setsstruct2  17135  strfv2d  17162  submre  17558  submrc  17585  isacs2  17610  coffth  17896  catcoppccl  18075  catcfuccl  18076  catcxpccl  18164  isdrs2  18263  fpwipodrs  18497  insubm  18777  sylow2a  19585  lsmmod  19641  lsmdisj  19647  lsmdisj2  19648  subgdisj1  19657  frgpnabllem1  19839  dmdprdd  19967  dprdfeq0  19990  dprdres  19996  dprddisj2  20007  dprd2da  20010  dmdprdsplit2lem  20013  ablfacrp  20034  pgpfac1lem3a  20044  pgpfac1lem3  20045  pgpfaclem1  20049  zrinitorngc  20610  zrtermorngc  20611  zrzeroorngc  20612  zrtermoringc  20643  zrninitoringc  20644  cntzsdrg  20770  2idl0  21250  2idl1  21251  zringlpirlem1  21452  zringlpirlem3  21454  irinitoringc  21469  nzerooringczr  21470  aspval  21862  mplind  22058  pmatcoe1fsupp  22676  baspartn  22929  bastg  22941  clsval2  23025  isopn3  23041  restbas  23133  lmss  23273  cmpcovf  23366  discmp  23373  cmpsublem  23374  cmpsub  23375  isconn2  23389  connclo  23390  llynlly  23452  restnlly  23457  restlly  23458  islly2  23459  llyrest  23460  nllyrest  23461  llyidm  23463  nllyidm  23464  hausllycmp  23469  cldllycmp  23470  lly1stc  23471  dislly  23472  llycmpkgen2  23525  1stckgenlem  23528  txlly  23611  txnlly  23612  txtube  23615  txcmplem1  23616  txcmplem2  23617  xkococnlem  23634  basqtop  23686  tgqtop  23687  infil  23838  fmfnfmlem4  23932  hauspwpwf1  23962  tgpconncompss  24089  ustfilxp  24188  metrest  24499  tgioo  24771  zdis  24792  icccmplem1  24798  icccmplem2  24799  reconnlem2  24803  xrge0tsms  24810  cnheibor  24932  cnllycmp  24933  ncvs1  25134  cphsqrtcl  25161  cmetcaulem  25265  ovollb2lem  25465  ovolctb  25467  ovolshftlem1  25486  ovolscalem1  25490  ovolicc1  25493  ioombl1lem1  25535  ioorf  25550  ioorcl  25554  dyadf  25568  vitalilem2  25586  vitali  25590  i1faddlem  25670  i1fmullem  25671  dvres2lem  25887  dvaddbr  25915  dvmulbr  25916  lhop1lem  25990  lhop  25993  dvcnvrelem2  25995  ig1peu  26150  tayl0  26338  rlimcnp2  26943  xrlimcnp  26945  ppisval  27081  ppisval2  27082  ppinprm  27129  chtnprm  27131  2sqlem7  27401  chebbnd1lem1  27446  footexALT  28800  footexlem2  28802  foot  28804  footne  28805  perprag  28808  colperpexlem3  28814  mideulem2  28816  lnopp2hpgb  28845  colopp  28851  lmieu  28866  lmimid  28876  hypcgrlem1  28881  hypcgrlem2  28882  trgcopyeulem  28887  f1otrg  28953  eengtrkg  29069  shuni  31386  5oalem1  31740  5oalem2  31741  5oalem4  31743  5oalem5  31744  3oalem2  31749  pjclem4  32285  pj3si  32293  ccatf1  33024  xrge0tsmsd  33149  wrdpmtrlast  33169  idlinsubrg  33506  ssdifidlprm  33533  qsdrngilem  33569  qsdrngi  33570  pidufd  33618  exsslsb  33756  lindsunlem  33784  lbsdiflsp0  33786  dimkerim  33787  irngss  33847  cmpcref  34010  cmppcmp  34018  dispcmp  34019  zarcmplem  34041  prsdm  34074  prsrn  34075  pnfneige0  34111  qqhucn  34152  rrhqima  34174  gsumesum  34219  esumcst  34223  esum2d  34253  sigainb  34296  inelpisys  34314  dynkin  34327  eulerpartlemgh  34538  eulerpartlemgs2  34540  eulerpartlemn  34541  sseqmw  34551  sseqf  34552  sseqp1  34555  fibp1  34561  bnj1379  34988  bnj1177  35164  cnllysconn  35443  rellysconn  35449  cvmsss2  35472  cvmcov2  35473  cvmopnlem  35476  mclsind  35768  weiunfr  36665  poimirlem30  37985  blbnd  38122  ssbnd  38123  heiborlem1  38146  heiborlem8  38153  heibor  38156  mndomgmid  38206  pmodlem1  40306  pclfinN  40360  mapdunirnN  42110  hdmaprnlem9N  42317  mhpind  43041  elrfi  43140  elrfirn  43141  fnwe2lem2  43497  dfac11  43508  kelac1  43509  kelac2lem  43510  dfac21  43512  islssfgi  43518  filnm  43536  lpirlnr  43563  hbtlem6  43575  hbt  43576  iocinico  43658  restuni3  45566  disjinfi  45640  iooabslt  45947  iocopn  45968  icoopn  45973  uzinico  46007  limciccioolb  46069  limcicciooub  46083  islpcn  46085  limcresioolb  46089  limcleqr  46090  limsuppnfdlem  46147  limsupresxr  46212  liminfresxr  46213  liminfvalxr  46229  liminflelimsupuz  46231  cnrefiisplem  46275  ioccncflimc  46331  icccncfext  46333  icocncflimc  46335  cncfiooicclem1  46339  itgiccshift  46426  itgperiod  46427  itgsbtaddcnst  46428  stoweidlem57  46503  fourierdlem20  46573  fourierdlem32  46585  fourierdlem33  46586  fourierdlem48  46600  fourierdlem49  46601  fourierdlem62  46614  fourierdlem71  46623  fouriersw  46677  qndenserrnbllem  46740  qndenserrn  46745  salgencntex  46789  fsumlesge0  46823  sge0tsms  46826  sge0cl  46827  sge0f1o  46828  sge0sup  46837  sge0resplit  46852  sge0iunmptlemre  46861  sge0fodjrnlem  46862  sge0rpcpnf  46867  sge0xaddlem1  46879  ovolval4lem2  47096  sssmf  47184  smflimlem3  47219  smfsuplem1  47257  fcores  47527  prproropf1olem2  47976  iinfconstbaslem  49552  ffthoppf  49652  uobeqw  49706  uobeq  49707  swapfiso  49772  swapciso  49773  fucoppcffth  49898  thincciso  49940  thinccisod  49941  termcterm  50000  termcterm2  50001  termcterm3  50002  termcciso  50003  termc2  50005  diagciso  50026  diagcic  50027  uobeqterm  50033