Theorem elind 4223

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

Syntax hints:   → wi 4   ∈ wcel 2108   ∩ cin 3975

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1540  df-ex 1778  df-sb 2065  df-clab 2718  df-cleq 2732  df-clel 2819  df-v 3490  df-in 3983

This theorem is referenced by:  fvelimad  6989  fnfvimad  7271  tfrlem5  8436  uniinqs  8855  unifpw  9425  f1opwfi  9426  fissuni  9427  fipreima  9428  elfir  9484  inelfi  9487  cantnfcl  9736  frrlem15  9826  tskwe  10019  infpwfidom  10097  infpwfien  10131  ackbij2lem1  10287  ackbij1lem3  10290  ackbij1lem4  10291  ackbij1lem6  10293  ackbij1lem11  10298  fin23lem24  10391  isfin1-3  10455  fpwwe2lem11  10710  fpwwe  10715  canthnumlem  10717  fz1isolem  14510  isprm7  16755  setsstruct2  17221  strfv2d  17249  submre  17663  submrc  17686  isacs2  17711  coffth  18003  catcoppccl  18184  catcoppcclOLD  18185  catcfuccl  18186  catcfucclOLD  18187  catcxpccl  18276  catcxpcclOLD  18277  isdrs2  18376  fpwipodrs  18610  insubm  18853  sylow2a  19661  lsmmod  19717  lsmdisj  19723  lsmdisj2  19724  subgdisj1  19733  frgpnabllem1  19915  dmdprdd  20043  dprdfeq0  20066  dprdres  20072  dprddisj2  20083  dprd2da  20086  dmdprdsplit2lem  20089  ablfacrp  20110  pgpfac1lem3a  20120  pgpfac1lem3  20121  pgpfaclem1  20125  zrinitorngc  20664  zrtermorngc  20665  zrzeroorngc  20666  zrtermoringc  20697  zrninitoringc  20698  cntzsdrg  20825  2idl0  21293  2idl1  21294  zringlpirlem1  21496  zringlpirlem3  21498  irinitoringc  21513  nzerooringczr  21514  aspval  21916  mplind  22117  pmatcoe1fsupp  22728  baspartn  22982  bastg  22994  clsval2  23079  isopn3  23095  restbas  23187  lmss  23327  cmpcovf  23420  discmp  23427  cmpsublem  23428  cmpsub  23429  isconn2  23443  connclo  23444  llynlly  23506  restnlly  23511  restlly  23512  islly2  23513  llyrest  23514  nllyrest  23515  llyidm  23517  nllyidm  23518  hausllycmp  23523  cldllycmp  23524  lly1stc  23525  dislly  23526  llycmpkgen2  23579  1stckgenlem  23582  txlly  23665  txnlly  23666  txtube  23669  txcmplem1  23670  txcmplem2  23671  xkococnlem  23688  basqtop  23740  tgqtop  23741  infil  23892  fmfnfmlem4  23986  hauspwpwf1  24016  tgpconncompss  24143  ustfilxp  24242  metrest  24558  tgioo  24837  zdis  24857  icccmplem1  24863  icccmplem2  24864  reconnlem2  24868  xrge0tsms  24875  cnheibor  25006  cnllycmp  25007  ncvs1  25210  cphsqrtcl  25237  cmetcaulem  25341  ovollb2lem  25542  ovolctb  25544  ovolshftlem1  25563  ovolscalem1  25567  ovolicc1  25570  ioombl1lem1  25612  ioorf  25627  ioorcl  25631  dyadf  25645  vitalilem2  25663  vitali  25667  i1faddlem  25747  i1fmullem  25748  dvres2lem  25965  dvaddbr  25994  dvmulbr  25995  dvmulbrOLD  25996  lhop1lem  26072  lhop  26075  dvcnvrelem2  26077  ig1peu  26234  tayl0  26421  rlimcnp2  27027  xrlimcnp  27029  ppisval  27165  ppisval2  27166  ppinprm  27213  chtnprm  27215  2sqlem7  27486  chebbnd1lem1  27531  footexALT  28744  footexlem2  28746  foot  28748  footne  28749  perprag  28752  colperpexlem3  28758  mideulem2  28760  lnopp2hpgb  28789  colopp  28795  lmieu  28810  lmimid  28820  hypcgrlem1  28825  hypcgrlem2  28826  trgcopyeulem  28831  f1otrg  28897  eengtrkg  29019  shuni  31332  5oalem1  31686  5oalem2  31687  5oalem4  31689  5oalem5  31690  3oalem2  31695  pjclem4  32231  pj3si  32239  ccatf1  32915  xrge0tsmsd  33041  wrdpmtrlast  33086  idlinsubrg  33424  ssdifidlprm  33451  qsdrngilem  33487  qsdrngi  33488  pidufd  33536  lindsunlem  33637  lbsdiflsp0  33639  dimkerim  33640  irngss  33687  cmpcref  33796  cmppcmp  33804  dispcmp  33805  zarcmplem  33827  prsdm  33860  prsrn  33861  pnfneige0  33897  qqhucn  33938  rrhqima  33960  gsumesum  34023  esumcst  34027  esum2d  34057  sigainb  34100  inelpisys  34118  dynkin  34131  eulerpartlemgh  34343  eulerpartlemgs2  34345  eulerpartlemn  34346  sseqmw  34356  sseqf  34357  sseqp1  34360  fibp1  34366  bnj1379  34806  bnj1177  34982  cnllysconn  35213  rellysconn  35219  cvmsss2  35242  cvmcov2  35243  cvmopnlem  35246  mclsind  35538  weiunfr  36433  poimirlem30  37610  blbnd  37747  ssbnd  37748  heiborlem1  37771  heiborlem8  37778  heibor  37781  mndomgmid  37831  pmodlem1  39803  pclfinN  39857  mapdunirnN  41607  hdmaprnlem9N  41814  mhpind  42549  elrfi  42650  elrfirn  42651  fnwe2lem2  43008  dfac11  43019  kelac1  43020  kelac2lem  43021  dfac21  43023  islssfgi  43029  filnm  43047  lpirlnr  43074  hbtlem6  43086  hbt  43087  iocinico  43173  restuni3  45020  disjinfi  45099  fvelima2  45169  iooabslt  45417  iocopn  45438  icoopn  45443  uzinico  45478  limciccioolb  45542  limcicciooub  45558  islpcn  45560  limcresioolb  45564  limcleqr  45565  limsuppnfdlem  45622  limsupresxr  45687  liminfresxr  45688  liminfvalxr  45704  liminflelimsupuz  45706  cnrefiisplem  45750  ioccncflimc  45806  icccncfext  45808  icocncflimc  45810  cncfiooicclem1  45814  itgiccshift  45901  itgperiod  45902  itgsbtaddcnst  45903  stoweidlem57  45978  fourierdlem20  46048  fourierdlem32  46060  fourierdlem33  46061  fourierdlem48  46075  fourierdlem49  46076  fourierdlem62  46089  fourierdlem71  46098  fouriersw  46152  qndenserrnbllem  46215  qndenserrn  46220  salgencntex  46264  fsumlesge0  46298  sge0tsms  46301  sge0cl  46302  sge0f1o  46303  sge0sup  46312  sge0resplit  46327  sge0iunmptlemre  46336  sge0fodjrnlem  46337  sge0rpcpnf  46342  sge0xaddlem1  46354  ovolval4lem2  46571  sssmf  46659  smflimlem3  46694  smfsuplem1  46732  fcores  46982  prproropf1olem2  47378  thincciso  48716