Theorem elind 4154

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

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

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-ext 2709

This theorem depends on definitions:  df-bi 207  df-an 396  df-tru 1545  df-ex 1782  df-sb 2069  df-clab 2716  df-cleq 2729  df-clel 2812  df-v 3444  df-in 3910

This theorem is referenced by:  fvelima2  6894  fvelimad  6909  fnfvimad  7190  tfrlem5  8321  uniinqs  8746  unifpw  9267  f1opwfi  9268  fissuni  9269  fipreima  9270  elfir  9330  inelfi  9333  cantnfcl  9588  frrlem15  9681  tskwe  9874  infpwfidom  9950  infpwfien  9984  ackbij2lem1  10140  ackbij1lem3  10143  ackbij1lem4  10144  ackbij1lem6  10146  ackbij1lem11  10151  fin23lem24  10244  isfin1-3  10308  fpwwe2lem11  10564  fpwwe  10569  canthnumlem  10571  fz1isolem  14396  isprm7  16647  setsstruct2  17113  strfv2d  17140  submre  17536  submrc  17563  isacs2  17588  coffth  17874  catcoppccl  18053  catcfuccl  18054  catcxpccl  18142  isdrs2  18241  fpwipodrs  18475  insubm  18755  sylow2a  19560  lsmmod  19616  lsmdisj  19622  lsmdisj2  19623  subgdisj1  19632  frgpnabllem1  19814  dmdprdd  19942  dprdfeq0  19965  dprdres  19971  dprddisj2  19982  dprd2da  19985  dmdprdsplit2lem  19988  ablfacrp  20009  pgpfac1lem3a  20019  pgpfac1lem3  20020  pgpfaclem1  20024  zrinitorngc  20587  zrtermorngc  20588  zrzeroorngc  20589  zrtermoringc  20620  zrninitoringc  20621  cntzsdrg  20747  2idl0  21227  2idl1  21228  zringlpirlem1  21429  zringlpirlem3  21431  irinitoringc  21446  nzerooringczr  21447  aspval  21840  mplind  22037  pmatcoe1fsupp  22657  baspartn  22910  bastg  22922  clsval2  23006  isopn3  23022  restbas  23114  lmss  23254  cmpcovf  23347  discmp  23354  cmpsublem  23355  cmpsub  23356  isconn2  23370  connclo  23371  llynlly  23433  restnlly  23438  restlly  23439  islly2  23440  llyrest  23441  nllyrest  23442  llyidm  23444  nllyidm  23445  hausllycmp  23450  cldllycmp  23451  lly1stc  23452  dislly  23453  llycmpkgen2  23506  1stckgenlem  23509  txlly  23592  txnlly  23593  txtube  23596  txcmplem1  23597  txcmplem2  23598  xkococnlem  23615  basqtop  23667  tgqtop  23668  infil  23819  fmfnfmlem4  23913  hauspwpwf1  23943  tgpconncompss  24070  ustfilxp  24169  metrest  24480  tgioo  24752  zdis  24773  icccmplem1  24779  icccmplem2  24780  reconnlem2  24784  xrge0tsms  24791  cnheibor  24922  cnllycmp  24923  ncvs1  25125  cphsqrtcl  25152  cmetcaulem  25256  ovollb2lem  25457  ovolctb  25459  ovolshftlem1  25478  ovolscalem1  25482  ovolicc1  25485  ioombl1lem1  25527  ioorf  25542  ioorcl  25546  dyadf  25560  vitalilem2  25578  vitali  25582  i1faddlem  25662  i1fmullem  25663  dvres2lem  25879  dvaddbr  25908  dvmulbr  25909  dvmulbrOLD  25910  lhop1lem  25986  lhop  25989  dvcnvrelem2  25991  ig1peu  26148  tayl0  26337  rlimcnp2  26944  xrlimcnp  26946  ppisval  27082  ppisval2  27083  ppinprm  27130  chtnprm  27132  2sqlem7  27403  chebbnd1lem1  27448  footexALT  28802  footexlem2  28804  foot  28806  footne  28807  perprag  28810  colperpexlem3  28816  mideulem2  28818  lnopp2hpgb  28847  colopp  28853  lmieu  28868  lmimid  28878  hypcgrlem1  28883  hypcgrlem2  28884  trgcopyeulem  28889  f1otrg  28955  eengtrkg  29071  shuni  31388  5oalem1  31742  5oalem2  31743  5oalem4  31745  5oalem5  31746  3oalem2  31751  pjclem4  32287  pj3si  32295  ccatf1  33042  xrge0tsmsd  33167  wrdpmtrlast  33187  idlinsubrg  33524  ssdifidlprm  33551  qsdrngilem  33587  qsdrngi  33588  pidufd  33636  exsslsb  33774  lindsunlem  33802  lbsdiflsp0  33804  dimkerim  33805  irngss  33865  cmpcref  34028  cmppcmp  34036  dispcmp  34037  zarcmplem  34059  prsdm  34092  prsrn  34093  pnfneige0  34129  qqhucn  34170  rrhqima  34192  gsumesum  34237  esumcst  34241  esum2d  34271  sigainb  34314  inelpisys  34332  dynkin  34345  eulerpartlemgh  34556  eulerpartlemgs2  34558  eulerpartlemn  34559  sseqmw  34569  sseqf  34570  sseqp1  34573  fibp1  34579  bnj1379  35006  bnj1177  35182  cnllysconn  35461  rellysconn  35467  cvmsss2  35490  cvmcov2  35491  cvmopnlem  35494  mclsind  35786  weiunfr  36683  poimirlem30  37901  blbnd  38038  ssbnd  38039  heiborlem1  38062  heiborlem8  38069  heibor  38072  mndomgmid  38122  pmodlem1  40222  pclfinN  40276  mapdunirnN  42026  hdmaprnlem9N  42233  mhpind  42952  elrfi  43051  elrfirn  43052  fnwe2lem2  43408  dfac11  43419  kelac1  43420  kelac2lem  43421  dfac21  43423  islssfgi  43429  filnm  43447  lpirlnr  43474  hbtlem6  43486  hbt  43487  iocinico  43569  restuni3  45477  disjinfi  45551  iooabslt  45859  iocopn  45880  icoopn  45885  uzinico  45919  limciccioolb  45981  limcicciooub  45995  islpcn  45997  limcresioolb  46001  limcleqr  46002  limsuppnfdlem  46059  limsupresxr  46124  liminfresxr  46125  liminfvalxr  46141  liminflelimsupuz  46143  cnrefiisplem  46187  ioccncflimc  46243  icccncfext  46245  icocncflimc  46247  cncfiooicclem1  46251  itgiccshift  46338  itgperiod  46339  itgsbtaddcnst  46340  stoweidlem57  46415  fourierdlem20  46485  fourierdlem32  46497  fourierdlem33  46498  fourierdlem48  46512  fourierdlem49  46513  fourierdlem62  46526  fourierdlem71  46535  fouriersw  46589  qndenserrnbllem  46652  qndenserrn  46657  salgencntex  46701  fsumlesge0  46735  sge0tsms  46738  sge0cl  46739  sge0f1o  46740  sge0sup  46749  sge0resplit  46764  sge0iunmptlemre  46773  sge0fodjrnlem  46774  sge0rpcpnf  46779  sge0xaddlem1  46791  ovolval4lem2  47008  sssmf  47096  smflimlem3  47131  smfsuplem1  47169  fcores  47427  prproropf1olem2  47864  iinfconstbaslem  49424  ffthoppf  49524  uobeqw  49578  uobeq  49579  swapfiso  49644  swapciso  49645  fucoppcffth  49770  thincciso  49812  thinccisod  49813  termcterm  49872  termcterm2  49873  termcterm3  49874  termcciso  49875  termc2  49877  diagciso  49898  diagcic  49899  uobeqterm  49905