Theorem elind 4171

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2793

This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-sb 2070  df-clab 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3496  df-in 3943

This theorem is referenced by:  fvelimad  6732  fnfvimad  6996  tfrlem5  8016  uniinqs  8377  unifpw  8827  f1opwfi  8828  fissuni  8829  fipreima  8830  elfir  8879  inelfi  8882  cantnfcl  9130  tskwe  9379  infpwfidom  9454  infpwfien  9488  ackbij2lem1  9641  ackbij1lem3  9644  ackbij1lem4  9645  ackbij1lem6  9647  ackbij1lem11  9652  fin23lem24  9744  isfin1-3  9808  fpwwe2lem12  10063  fpwwe  10068  canthnumlem  10070  fz1isolem  13820  isprm7  16052  setsstruct2  16521  strfv2d  16529  submre  16876  submrc  16899  isacs2  16924  coffth  17206  catcoppccl  17368  catcfuccl  17369  catcxpccl  17457  isdrs2  17549  fpwipodrs  17774  insubm  17983  sylow2a  18744  lsmmod  18801  lsmdisj  18807  lsmdisj2  18808  subgdisj1  18817  frgpnabllem1  18993  dmdprdd  19121  dprdfeq0  19144  dprdres  19150  dprddisj2  19161  dprd2da  19164  dmdprdsplit2lem  19167  ablfacrp  19188  pgpfac1lem3a  19198  pgpfac1lem3  19199  pgpfaclem1  19203  cntzsdrg  19581  aspval  20102  mplind  20282  zringlpirlem1  20631  zringlpirlem3  20633  pmatcoe1fsupp  21309  baspartn  21562  bastg  21574  clsval2  21658  isopn3  21674  restbas  21766  lmss  21906  cmpcovf  21999  discmp  22006  cmpsublem  22007  cmpsub  22008  isconn2  22022  connclo  22023  llynlly  22085  restnlly  22090  restlly  22091  islly2  22092  llyrest  22093  nllyrest  22094  llyidm  22096  nllyidm  22097  hausllycmp  22102  cldllycmp  22103  lly1stc  22104  dislly  22105  llycmpkgen2  22158  1stckgenlem  22161  txlly  22244  txnlly  22245  txtube  22248  txcmplem1  22249  txcmplem2  22250  xkococnlem  22267  basqtop  22319  tgqtop  22320  infil  22471  fmfnfmlem4  22565  hauspwpwf1  22595  tgpconncompss  22722  ustfilxp  22821  metrest  23134  tgioo  23404  zdis  23424  icccmplem1  23430  icccmplem2  23431  reconnlem2  23435  xrge0tsms  23442  cnheibor  23559  cnllycmp  23560  ncvs1  23761  cphsqrtcl  23788  cmetcaulem  23891  ovollb2lem  24089  ovolctb  24091  ovolshftlem1  24110  ovolscalem1  24114  ovolicc1  24117  ioombl1lem1  24159  ioorf  24174  ioorcl  24178  dyadf  24192  vitalilem2  24210  vitali  24214  i1faddlem  24294  i1fmullem  24295  dvres2lem  24508  dvaddbr  24535  dvmulbr  24536  lhop1lem  24610  lhop  24613  dvcnvrelem2  24615  ig1peu  24765  tayl0  24950  rlimcnp2  25544  xrlimcnp  25546  ppisval  25681  ppisval2  25682  ppinprm  25729  chtnprm  25731  2sqlem7  26000  chebbnd1lem1  26045  footexALT  26504  footexlem2  26506  foot  26508  footne  26509  perprag  26512  colperpexlem3  26518  mideulem2  26520  lnopp2hpgb  26549  colopp  26555  lmieu  26570  lmimid  26580  hypcgrlem1  26585  hypcgrlem2  26586  trgcopyeulem  26591  f1otrg  26657  eengtrkg  26772  shuni  29077  5oalem1  29431  5oalem2  29432  5oalem4  29434  5oalem5  29435  3oalem2  29440  pjclem4  29976  pj3si  29984  ccatf1  30625  xrge0tsmsd  30692  lindsunlem  31020  lbsdiflsp0  31022  dimkerim  31023  cmpcref  31114  cmppcmp  31122  dispcmp  31123  prsdm  31157  prsrn  31158  pnfneige0  31194  qqhucn  31233  rrhqima  31255  gsumesum  31318  esumcst  31322  esum2d  31352  sigainb  31395  inelpisys  31413  dynkin  31426  eulerpartlemgh  31636  eulerpartlemgs2  31638  eulerpartlemn  31639  sseqmw  31649  sseqf  31650  sseqp1  31653  fibp1  31659  bnj1379  32102  bnj1177  32278  cnllysconn  32492  rellysconn  32498  cvmsss2  32521  cvmcov2  32522  cvmopnlem  32525  mclsind  32817  frrlem15  33142  poimirlem30  34937  blbnd  35080  ssbnd  35081  heiborlem1  35104  heiborlem8  35111  heibor  35114  mndomgmid  35164  pmodlem1  36997  pclfinN  37051  mapdunirnN  38801  hdmaprnlem9N  39008  elrfi  39340  elrfirn  39341  fnwe2lem2  39700  dfac11  39711  kelac1  39712  kelac2lem  39713  dfac21  39715  islssfgi  39721  filnm  39739  lpirlnr  39766  hbtlem6  39778  hbt  39779  iocinico  39867  restuni3  41433  disjinfi  41503  fvelima2  41581  iooabslt  41823  iocopn  41845  icoopn  41850  uzinico  41885  limciccioolb  41951  limcicciooub  41967  islpcn  41969  limcresioolb  41973  limcleqr  41974  limsuppnfdlem  42031  limsupresxr  42096  liminfresxr  42097  liminfvalxr  42113  liminflelimsupuz  42115  cnrefiisplem  42159  ioccncflimc  42217  icccncfext  42219  icocncflimc  42221  cncfiooicclem1  42225  itgiccshift  42314  itgperiod  42315  itgsbtaddcnst  42316  stoweidlem57  42391  fourierdlem20  42461  fourierdlem32  42473  fourierdlem33  42474  fourierdlem48  42488  fourierdlem49  42489  fourierdlem62  42502  fourierdlem71  42511  fouriersw  42565  qndenserrnbllem  42628  qndenserrn  42633  salgencntex  42675  fsumlesge0  42708  sge0tsms  42711  sge0cl  42712  sge0f1o  42713  sge0sup  42722  sge0resplit  42737  sge0iunmptlemre  42746  sge0fodjrnlem  42747  sge0rpcpnf  42752  sge0xaddlem1  42764  ovolval4lem2  42981  sssmf  43064  smflimlem3  43098  smfsuplem1  43134  prproropf1olem2  43715  zrinitorngc  44320  zrtermorngc  44321  zrzeroorngc  44322  irinitoringc  44389  zrtermoringc  44390  zrninitoringc  44391  nzerooringczr  44392