Theorem elind 4161

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

Syntax hints:   → wi 4   ∈ wcel 2149   ∩ cin 3912

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1822  ax-4 1836  ax-5 1937  ax-6 1994  ax-7 2035  ax-8 2151  ax-9 2159  ax-ext 2741

This theorem depends on definitions:  df-bi 210  df-an 401  df-tru 1570  df-ex 1807  df-sb 2098  df-clab 2748  df-cleq 2761  df-clel 2844  df-v 3465  df-in 3920

This theorem is referenced by:  fvelima2  6931  fvelimad  6946  fnfvimad  7230  tfrlem5  8362  uniinqs  8791  unifpw  9308  f1opwfi  9309  fissuni  9310  fipreima  9311  elfir  9371  inelfi  9374  cantnfcl  9632  frrlem15  9725  tskwe  9932  infpwfidom  10008  infpwfien  10042  ackbij2lem1  10197  ackbij1lem3  10200  ackbij1lem4  10201  ackbij1lem6  10203  ackbij1lem11  10208  fin23lem24  10302  isfin1-3  10366  fpwwe2lem11  10622  fpwwe  10627  canthnumlem  10629  fz1isolem  14494  isprm7  16763  setsstruct2  17230  strfv2d  17257  submre  17653  submrc  17680  isacs2  17705  coffth  17991  catcoppccl  18170  catcfuccl  18171  catcxpccl  18259  isdrs2  18358  fpwipodrs  18592  insubm  18873  sylow2a  19685  lsmmod  19741  lsmdisj  19747  lsmdisj2  19748  subgdisj1  19757  frgpnabllem1  19939  dmdprdd  20067  dprdfeq0  20090  dprdres  20096  dprddisj2  20107  dprd2da  20110  dmdprdsplit2lem  20113  ablfacrp  20134  pgpfac1lem3a  20144  pgpfac1lem3  20145  pgpfaclem1  20149  zrinitorngc  20723  zrtermorngc  20724  zrzeroorngc  20725  zrtermoringc  20756  zrninitoringc  20757  cntzsdrg  20879  2idl0  21366  2idl1  21367  ssdifidlprm  21451  zringlpirlem1  21577  zringlpirlem3  21579  irinitoringc  21594  nzerooringczr  21595  aspval  21987  mplind  22186  pmatcoe1fsupp  22823  baspartn  23076  bastg  23088  clsval2  23172  isopn3  23188  restbas  23280  lmss  23420  cmpcovf  23513  discmp  23520  cmpsublem  23521  cmpsub  23522  isconn2  23536  connclo  23537  llynlly  23599  restnlly  23604  restlly  23605  islly2  23606  llyrest  23607  nllyrest  23608  llyidm  23610  nllyidm  23611  hausllycmp  23616  cldllycmp  23617  lly1stc  23618  dislly  23619  llycmpkgen2  23672  1stckgenlem  23675  txlly  23758  txnlly  23759  txtube  23762  txcmplem1  23763  txcmplem2  23764  xkococnlem  23781  basqtop  23833  tgqtop  23834  infil  23985  fmfnfmlem4  24079  hauspwpwf1  24109  tgpconncompss  24236  ustfilxp  24335  metrest  24646  tgioo  24918  zdis  24939  icccmplem1  24945  icccmplem2  24946  reconnlem2  24950  xrge0tsms  24957  cnheibor  25079  cnllycmp  25080  ncvs1  25281  cphsqrtcl  25308  cmetcaulem  25412  ovollb2lem  25612  ovolctb  25614  ovolshftlem1  25633  ovolscalem1  25637  ovolicc1  25640  ioombl1lem1  25682  ioorf  25697  ioorcl  25701  dyadf  25715  vitalilem2  25733  vitali  25737  i1faddlem  25817  i1fmullem  25818  dvres2lem  26034  dvaddbr  26062  dvmulbr  26063  lhop1lem  26137  lhop  26140  dvcnvrelem2  26142  ig1peu  26297  tayl0  26487  rlimcnp2  27093  xrlimcnp  27095  ppisval  27230  ppisval2  27231  ppinprm  27278  chtnprm  27280  2sqlem7  27550  chebbnd1lem1  27595  tglnpt4  28886  footexALT  28953  footexlem2  28955  foot  28957  footne  28958  perprag  28962  colperpexlem3  28968  mideulem2  28970  lnopp2hpgb  29000  colopp  29006  lnincplng  29020  plngrotlem1  29023  plngrotlem2  29024  lnssplng  29028  lmieu  29047  lmimid  29057  hypcgrlem1  29062  hypcgrlem2  29063  trgcopyeulem  29069  prlngmolem1  29151  prlngmolem2  29152  f1otrg  29157  eengtrkg  29273  shuni  31589  5oalem1  31943  5oalem2  31944  5oalem4  31946  5oalem5  31947  3oalem2  31952  pjclem4  32488  pj3si  32496  ccatf1  33206  xrge0tsmsd  33330  wrdpmtrlast  33350  idlinsubrg  33679  qsdrngilem  33717  qsdrngi  33718  pidufd  33774  exsslsb  33928  lindsunlem  33955  lbsdiflsp0  33957  dimkerim  33958  irngss  34018  cmpcref  34181  cmppcmp  34189  dispcmp  34190  zarcmplem  34212  prsdm  34245  prsrn  34246  pnfneige0  34282  qqhucn  34323  rrhqima  34345  gsumesum  34390  esumcst  34394  esum2d  34424  sigainb  34467  inelpisys  34485  dynkin  34498  eulerpartlemgh  34709  eulerpartlemgs2  34711  eulerpartlemn  34712  sseqmw  34722  sseqf  34723  sseqp1  34726  fibp1  34732  bnj1379  35159  bnj1177  35335  cnllysconn  35632  rellysconn  35638  cvmsss2  35661  cvmcov2  35662  cvmopnlem  35665  mclsind  35957  weiunfr  36863  poimirlem30  38184  blbnd  38321  ssbnd  38322  heiborlem1  38345  heiborlem8  38352  heibor  38355  mndomgmid  38405  pmodlem1  40505  pclfinN  40559  mapdunirnN  42309  hdmaprnlem9N  42516  mhpind  43213  elrfi  43312  elrfirn  43313  fnwe2lem2  43665  dfac11  43676  kelac1  43677  kelac2lem  43678  dfac21  43680  islssfgi  43686  filnm  43704  lpirlnr  43731  hbtlem6  43743  hbt  43744  iocinico  43826  restuni3  45723  disjinfi  45797  iooabslt  46102  iocopn  46123  icoopn  46128  uzinico  46162  limciccioolb  46224  limcicciooub  46238  islpcn  46240  limcresioolb  46244  limcleqr  46245  limsuppnfdlem  46302  limsupresxr  46367  liminfresxr  46368  liminfvalxr  46384  liminflelimsupuz  46386  cnrefiisplem  46430  ioccncflimc  46486  icccncfext  46488  icocncflimc  46490  cncfiooicclem1  46494  itgiccshift  46581  itgperiod  46582  itgsbtaddcnst  46583  stoweidlem57  46658  fourierdlem20  46728  fourierdlem32  46740  fourierdlem33  46741  fourierdlem48  46755  fourierdlem49  46756  fourierdlem62  46769  fourierdlem71  46778  fouriersw  46832  qndenserrnbllem  46895  qndenserrn  46900  salgencntex  46944  fsumlesge0  46978  sge0tsms  46981  sge0cl  46982  sge0f1o  46983  sge0sup  46992  sge0resplit  47007  sge0iunmptlemre  47016  sge0fodjrnlem  47017  sge0rpcpnf  47022  sge0xaddlem1  47034  ovolval4lem2  47251  sssmf  47339  smflimlem3  47374  smfsuplem1  47412  fcores  47688  prproropf1olem2  48137  iinfconstbaslem  49723  ffthoppf  49823  uobeqw  49877  uobeq  49878  swapfiso  49943  swapciso  49944  fucoppcffth  50069  thincciso  50111  thinccisod  50112  termcterm  50171  termcterm2  50172  termcterm3  50173  termcciso  50174  termc2  50176  diagciso  50197  diagcic  50198  uobeqterm  50204