Theorem elind 4146

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

This proof depends on syntax axioms:   → wi 4   ∈ wcel 2145   ∩ cin 3898

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1828  ax-4 1842  ax-5 1943  ax-6 2000  ax-7 2041  ax-8 2147  ax-9 2155  ax-ext 2732

This proof depends on definitions:  df-bi 210  df-an 402  df-tru 1573  df-ex 1813  df-sb 2100  df-clab 2739  df-cleq 2752  df-clel 2835  df-v 3452  df-in 3906

This theorem is used by:  fvelima2  6930  fvelimad  6945  fnfvimad  7233  tfrlem5  8368  uniinqs  8797  unifpw  9322  f1opwfi  9323  fissuni  9324  fipreima  9325  elfir  9385  inelfi  9388  cantnfcl  9646  frrlem15  9739  tskwe  9955  infpwfidom  10031  infpwfien  10065  ackbij2lem1  10220  ackbij1lem3  10223  ackbij1lem4  10224  ackbij1lem6  10226  ackbij1lem11  10231  fin23lem24  10324  isfin1-3  10388  fpwwe2lem11  10650  fpwwe  10655  canthnumlem  10657  fz1isolem  14526  ccatf1  14656  isprm7  16799  setsstruct2  17266  strfv2d  17293  submre  17689  submrc  17716  isacs2  17741  coffth  18027  catcoppccl  18206  catcfuccl  18207  catcxpccl  18295  isdrs2  18394  fpwipodrs  18628  insubm  18927  sylow2a  19746  lsmmod  19802  lsmdisj  19808  lsmdisj2  19809  subgdisj1  19818  frgpnabllem1  20000  dmdprdd  20128  dprdfeq0  20151  dprdres  20157  dprddisj2  20168  dprd2da  20171  dmdprdsplit2lem  20174  ablfacrp  20195  pgpfac1lem3a  20205  pgpfac1lem3  20206  pgpfaclem1  20210  zrinitorngc  20804  zrtermorngc  20805  zrzeroorngc  20806  zrtermoringc  20837  zrninitoringc  20838  cntzsdrg  20968  2idl0  21462  2idl1  21463  ssdifidlprm  21549  zringlpirlem1  21675  zringlpirlem3  21677  irinitoringc  21692  nzerooringczr  21693  aspval  22087  mplind  22286  pmatcoe1fsupp  22926  baspartn  23179  bastg  23191  clsval2  23275  isopn3  23291  restbas  23383  lmss  23523  cmpcovf  23616  discmp  23623  cmpsublem  23624  cmpsub  23625  isconn2  23639  connclo  23640  llynlly  23703  restnlly  23708  restlly  23709  islly2  23710  llyrest  23711  nllyrest  23712  llyidm  23714  nllyidm  23715  hausllycmp  23720  cldllycmp  23721  lly1stc  23722  dislly  23723  llycmpkgen2  23776  1stckgenlem  23779  txlly  23862  txnlly  23863  txtube  23866  txcmplem1  23867  txcmplem2  23868  xkococnlem  23885  basqtop  23937  tgqtop  23938  infil  24089  fmfnfmlem4  24183  hauspwpwf1  24213  tgpconncompss  24340  ustfilxp  24439  metrest  24750  tgioo  25022  zdis  25043  icccmplem1  25049  icccmplem2  25050  reconnlem2  25054  xrge0tsms  25061  cnheibor  25183  cnllycmp  25184  ncvs1  25385  cphsqrtcl  25412  cmetcaulem  25516  ovollb2lem  25716  ovolctb  25718  ovolshftlem1  25737  ovolscalem1  25741  ovolicc1  25744  ioombl1lem1  25786  ioorf  25801  ioorcl  25805  dyadf  25819  vitalilem2  25837  vitali  25841  i1faddlem  25921  i1fmullem  25922  dvres2lem  26137  dvaddbr  26165  dvmulbr  26166  lhop1lem  26240  lhop  26243  dvcnvrelem2  26245  ig1peu  26400  tayl0  26598  rlimcnp2  27203  xrlimcnp  27205  ppisval  27340  ppisval2  27341  ppinprm  27388  chtnprm  27390  2sqlem7  27660  chebbnd1lem1  27705  tglnpt4  29002  footexALT  29072  footexlem2  29074  foot  29076  footne  29077  perprag  29081  colperpexlem3  29087  mideulem2  29089  lnoppinn0  29110  lnopp2hpgb  29120  colopp  29126  lnincplng  29141  plngrotlem1  29144  plngrotlem2  29145  lnssplng  29149  lmieu  29168  lmimid  29178  hypcgrlem1  29184  hypcgrlem2  29185  trgcopyeulem  29191  tgaaddcpbllem1  29228  tgaaddcpbl  29231  angmgmaddeu2  29259  angmgmaddeu3  29260  angmgmaddov2lem  29266  angmgmaddcpbl  29269  angmgmaddrid  29272  dfprlng2  29304  prlngmolem1  29309  prlngmolem2  29310  prlngmo2  29313  prlngpln4  29315  prlngmid2  29318  prlngsymquadlem  29320  quadcgrprlng  29323  f1otrg  29327  eengtrkg  29443  shuni  31781  5oalem1  32135  5oalem2  32136  5oalem4  32138  5oalem5  32139  3oalem2  32144  pjclem4  32680  pj3si  32688  xrge0tsmsd  33513  wrdpmtrlast  33533  idlinsubrg  33859  qsdrngilem  33896  qsdrngi  33897  pidufd  33953  exsslsb  34107  lindsunlem  34134  lbsdiflsp0  34136  dimkerim  34137  irngss  34197  cmpcref  34360  cmppcmp  34368  dispcmp  34369  zarcmplem  34391  prsdm  34424  prsrn  34425  pnfneige0  34461  qqhucn  34502  rrhqima  34524  gsumesum  34569  esumcst  34573  esum2d  34603  sigainb  34647  inelpisys  34665  dynkin  34678  eulerpartlemgh  34889  eulerpartlemgs2  34891  eulerpartlemn  34892  sseqmw  34902  sseqf  34903  sseqp1  34906  fibp1  34912  bnj1379  35339  bnj1177  35515  cnllysconn  35824  rellysconn  35830  cvmsss2  35853  cvmcov2  35854  cvmopnlem  35857  mclsind  36149  weiunfr  37086  poimirlem30  38399  blbnd  38537  ssbnd  38538  heiborlem1  38561  heiborlem8  38568  heibor  38571  mndomgmid  38621  pmodlem1  40719  pclfinN  40773  mapdunirnN  42523  hdmaprnlem9N  42730  mhpind  43440  elrfi  43539  elrfirn  43540  fnwe2lem2  43892  dfac11  43903  kelac1  43904  kelac2lem  43905  dfac21  43907  islssfgi  43913  filnm  43931  lpirlnr  43958  hbtlem6  43970  hbt  43971  iocinico  44053  restuni3  45950  disjinfi  46024  iooabslt  46329  iocopn  46350  icoopn  46355  uzinico  46389  limciccioolb  46451  limcicciooub  46465  islpcn  46467  limcresioolb  46471  limcleqr  46472  limsuppnfdlem  46529  limsupresxr  46594  liminfresxr  46595  liminfvalxr  46611  liminflelimsupuz  46613  cnrefiisplem  46657  ioccncflimc  46713  icccncfext  46715  icocncflimc  46717  cncfiooicclem1  46721  itgiccshift  46808  itgperiod  46809  itgsbtaddcnst  46810  stoweidlem57  46885  fourierdlem20  46955  fourierdlem32  46967  fourierdlem33  46968  fourierdlem48  46982  fourierdlem49  46983  fourierdlem62  46996  fourierdlem71  47005  fouriersw  47059  qndenserrnbllem  47122  qndenserrn  47127  salgencntex  47171  fsumlesge0  47205  sge0tsms  47208  sge0cl  47209  sge0f1o  47210  sge0sup  47219  sge0resplit  47234  sge0iunmptlemre  47243  sge0fodjrnlem  47244  sge0rpcpnf  47249  sge0xaddlem1  47261  ovolval4lem2  47478  sssmf  47566  smflimlem3  47601  smfsuplem1  47639  fcores  47955  prproropf1olem2  48404  iinfconstbaslem  49991  ffthoppf  50091  uobeqw  50145  uobeq  50146  swapfiso  50211  swapciso  50212  fucoppcffth  50337  thincciso  50379  thinccisod  50380  termcterm  50439  termcterm2  50440  termcterm3  50441  termcciso  50442  termc2  50444  diagciso  50465  diagcic  50466  uobeqterm  50472