Theorem elind 4145

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

Syntax hints:   → wi 4   ∈ wcel 2111   ∩ cin 3896

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 1968  ax-7 2009  ax-8 2113  ax-9 2121  ax-ext 2703

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1544  df-ex 1781  df-sb 2068  df-clab 2710  df-cleq 2723  df-clel 2806  df-v 3438  df-in 3904

This theorem is referenced by:  fvelima2  6869  fvelimad  6884  fnfvimad  7163  tfrlem5  8294  uniinqs  8716  unifpw  9234  f1opwfi  9235  fissuni  9236  fipreima  9237  elfir  9294  inelfi  9297  cantnfcl  9552  frrlem15  9645  tskwe  9838  infpwfidom  9914  infpwfien  9948  ackbij2lem1  10104  ackbij1lem3  10107  ackbij1lem4  10108  ackbij1lem6  10110  ackbij1lem11  10115  fin23lem24  10208  isfin1-3  10272  fpwwe2lem11  10527  fpwwe  10532  canthnumlem  10534  fz1isolem  14363  isprm7  16614  setsstruct2  17080  strfv2d  17107  submre  17502  submrc  17529  isacs2  17554  coffth  17840  catcoppccl  18019  catcfuccl  18020  catcxpccl  18108  isdrs2  18207  fpwipodrs  18441  insubm  18721  sylow2a  19526  lsmmod  19582  lsmdisj  19588  lsmdisj2  19589  subgdisj1  19598  frgpnabllem1  19780  dmdprdd  19908  dprdfeq0  19931  dprdres  19937  dprddisj2  19948  dprd2da  19951  dmdprdsplit2lem  19954  ablfacrp  19975  pgpfac1lem3a  19985  pgpfac1lem3  19986  pgpfaclem1  19990  zrinitorngc  20552  zrtermorngc  20553  zrzeroorngc  20554  zrtermoringc  20585  zrninitoringc  20586  cntzsdrg  20712  2idl0  21192  2idl1  21193  zringlpirlem1  21394  zringlpirlem3  21396  irinitoringc  21411  nzerooringczr  21412  aspval  21805  mplind  22000  pmatcoe1fsupp  22611  baspartn  22864  bastg  22876  clsval2  22960  isopn3  22976  restbas  23068  lmss  23208  cmpcovf  23301  discmp  23308  cmpsublem  23309  cmpsub  23310  isconn2  23324  connclo  23325  llynlly  23387  restnlly  23392  restlly  23393  islly2  23394  llyrest  23395  nllyrest  23396  llyidm  23398  nllyidm  23399  hausllycmp  23404  cldllycmp  23405  lly1stc  23406  dislly  23407  llycmpkgen2  23460  1stckgenlem  23463  txlly  23546  txnlly  23547  txtube  23550  txcmplem1  23551  txcmplem2  23552  xkococnlem  23569  basqtop  23621  tgqtop  23622  infil  23773  fmfnfmlem4  23867  hauspwpwf1  23897  tgpconncompss  24024  ustfilxp  24123  metrest  24434  tgioo  24706  zdis  24727  icccmplem1  24733  icccmplem2  24734  reconnlem2  24738  xrge0tsms  24745  cnheibor  24876  cnllycmp  24877  ncvs1  25079  cphsqrtcl  25106  cmetcaulem  25210  ovollb2lem  25411  ovolctb  25413  ovolshftlem1  25432  ovolscalem1  25436  ovolicc1  25439  ioombl1lem1  25481  ioorf  25496  ioorcl  25500  dyadf  25514  vitalilem2  25532  vitali  25536  i1faddlem  25616  i1fmullem  25617  dvres2lem  25833  dvaddbr  25862  dvmulbr  25863  dvmulbrOLD  25864  lhop1lem  25940  lhop  25943  dvcnvrelem2  25945  ig1peu  26102  tayl0  26291  rlimcnp2  26898  xrlimcnp  26900  ppisval  27036  ppisval2  27037  ppinprm  27084  chtnprm  27086  2sqlem7  27357  chebbnd1lem1  27402  footexALT  28691  footexlem2  28693  foot  28695  footne  28696  perprag  28699  colperpexlem3  28705  mideulem2  28707  lnopp2hpgb  28736  colopp  28742  lmieu  28757  lmimid  28767  hypcgrlem1  28772  hypcgrlem2  28773  trgcopyeulem  28778  f1otrg  28844  eengtrkg  28959  shuni  31272  5oalem1  31626  5oalem2  31627  5oalem4  31629  5oalem5  31630  3oalem2  31635  pjclem4  32171  pj3si  32179  ccatf1  32922  xrge0tsmsd  33034  wrdpmtrlast  33054  idlinsubrg  33388  ssdifidlprm  33415  qsdrngilem  33451  qsdrngi  33452  pidufd  33500  exsslsb  33601  lindsunlem  33629  lbsdiflsp0  33631  dimkerim  33632  irngss  33692  cmpcref  33855  cmppcmp  33863  dispcmp  33864  zarcmplem  33886  prsdm  33919  prsrn  33920  pnfneige0  33956  qqhucn  33997  rrhqima  34019  gsumesum  34064  esumcst  34068  esum2d  34098  sigainb  34141  inelpisys  34159  dynkin  34172  eulerpartlemgh  34383  eulerpartlemgs2  34385  eulerpartlemn  34386  sseqmw  34396  sseqf  34397  sseqp1  34400  fibp1  34406  bnj1379  34834  bnj1177  35010  cnllysconn  35281  rellysconn  35287  cvmsss2  35310  cvmcov2  35311  cvmopnlem  35314  mclsind  35606  weiunfr  36501  poimirlem30  37690  blbnd  37827  ssbnd  37828  heiborlem1  37851  heiborlem8  37858  heibor  37861  mndomgmid  37911  pmodlem1  39885  pclfinN  39939  mapdunirnN  41689  hdmaprnlem9N  41896  mhpind  42627  elrfi  42727  elrfirn  42728  fnwe2lem2  43084  dfac11  43095  kelac1  43096  kelac2lem  43097  dfac21  43099  islssfgi  43105  filnm  43123  lpirlnr  43150  hbtlem6  43162  hbt  43163  iocinico  43245  restuni3  45155  disjinfi  45229  iooabslt  45539  iocopn  45560  icoopn  45565  uzinico  45599  limciccioolb  45661  limcicciooub  45675  islpcn  45677  limcresioolb  45681  limcleqr  45682  limsuppnfdlem  45739  limsupresxr  45804  liminfresxr  45805  liminfvalxr  45821  liminflelimsupuz  45823  cnrefiisplem  45867  ioccncflimc  45923  icccncfext  45925  icocncflimc  45927  cncfiooicclem1  45931  itgiccshift  46018  itgperiod  46019  itgsbtaddcnst  46020  stoweidlem57  46095  fourierdlem20  46165  fourierdlem32  46177  fourierdlem33  46178  fourierdlem48  46192  fourierdlem49  46193  fourierdlem62  46206  fourierdlem71  46215  fouriersw  46269  qndenserrnbllem  46332  qndenserrn  46337  salgencntex  46381  fsumlesge0  46415  sge0tsms  46418  sge0cl  46419  sge0f1o  46420  sge0sup  46429  sge0resplit  46444  sge0iunmptlemre  46453  sge0fodjrnlem  46454  sge0rpcpnf  46459  sge0xaddlem1  46471  ovolval4lem2  46688  sssmf  46776  smflimlem3  46811  smfsuplem1  46849  fcores  47098  prproropf1olem2  47535  iinfconstbaslem  49097  ffthoppf  49197  uobeqw  49251  uobeq  49252  swapfiso  49317  swapciso  49318  fucoppcffth  49443  thincciso  49485  thinccisod  49486  termcterm  49545  termcterm2  49546  termcterm3  49547  termcciso  49548  termc2  49550  diagciso  49571  diagcic  49572  uobeqterm  49578