Theorem elind 4150

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

Syntax hints:   → wi 4   ∈ wcel 2141   ∩ cin 3901

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-tru 1562  df-ex 1799  df-sb 2090  df-clab 2740  df-cleq 2753  df-clel 2836  df-v 3455  df-in 3909

This theorem is referenced by:  fvelima2  6914  fvelimad  6929  fnfvimad  7213  tfrlem5  8344  uniinqs  8773  unifpw  9292  f1opwfi  9293  fissuni  9294  fipreima  9295  elfir  9355  inelfi  9358  cantnfcl  9616  frrlem15  9709  tskwe  9902  infpwfidom  9978  infpwfien  10012  ackbij2lem1  10168  ackbij1lem3  10171  ackbij1lem4  10172  ackbij1lem6  10174  ackbij1lem11  10179  fin23lem24  10273  isfin1-3  10337  fpwwe2lem11  10593  fpwwe  10598  canthnumlem  10600  fz1isolem  14468  isprm7  16734  setsstruct2  17201  strfv2d  17228  submre  17624  submrc  17651  isacs2  17676  coffth  17962  catcoppccl  18141  catcfuccl  18142  catcxpccl  18230  isdrs2  18329  fpwipodrs  18563  insubm  18843  sylow2a  19650  lsmmod  19706  lsmdisj  19712  lsmdisj2  19713  subgdisj1  19722  frgpnabllem1  19904  dmdprdd  20032  dprdfeq0  20055  dprdres  20061  dprddisj2  20072  dprd2da  20075  dmdprdsplit2lem  20078  ablfacrp  20099  pgpfac1lem3a  20109  pgpfac1lem3  20110  pgpfaclem1  20114  zrinitorngc  20679  zrtermorngc  20680  zrzeroorngc  20681  zrtermoringc  20712  zrninitoringc  20713  cntzsdrg  20839  2idl0  21318  2idl1  21319  zringlpirlem1  21502  zringlpirlem3  21504  irinitoringc  21519  nzerooringczr  21520  aspval  21912  mplind  22111  pmatcoe1fsupp  22749  baspartn  23002  bastg  23014  clsval2  23098  isopn3  23114  restbas  23206  lmss  23346  cmpcovf  23439  discmp  23446  cmpsublem  23447  cmpsub  23448  isconn2  23462  connclo  23463  llynlly  23525  restnlly  23530  restlly  23531  islly2  23532  llyrest  23533  nllyrest  23534  llyidm  23536  nllyidm  23537  hausllycmp  23542  cldllycmp  23543  lly1stc  23544  dislly  23545  llycmpkgen2  23598  1stckgenlem  23601  txlly  23684  txnlly  23685  txtube  23688  txcmplem1  23689  txcmplem2  23690  xkococnlem  23707  basqtop  23759  tgqtop  23760  infil  23911  fmfnfmlem4  24005  hauspwpwf1  24035  tgpconncompss  24162  ustfilxp  24261  metrest  24572  tgioo  24844  zdis  24865  icccmplem1  24871  icccmplem2  24872  reconnlem2  24876  xrge0tsms  24883  cnheibor  25005  cnllycmp  25006  ncvs1  25207  cphsqrtcl  25234  cmetcaulem  25338  ovollb2lem  25538  ovolctb  25540  ovolshftlem1  25559  ovolscalem1  25563  ovolicc1  25566  ioombl1lem1  25608  ioorf  25623  ioorcl  25627  dyadf  25641  vitalilem2  25659  vitali  25663  i1faddlem  25743  i1fmullem  25744  dvres2lem  25960  dvaddbr  25988  dvmulbr  25989  lhop1lem  26063  lhop  26066  dvcnvrelem2  26068  ig1peu  26223  tayl0  26413  rlimcnp2  27019  xrlimcnp  27021  ppisval  27156  ppisval2  27157  ppinprm  27204  chtnprm  27206  2sqlem7  27476  chebbnd1lem1  27521  footexALT  28875  footexlem2  28877  foot  28879  footne  28880  perprag  28883  colperpexlem3  28889  mideulem2  28891  lnopp2hpgb  28920  colopp  28926  lmieu  28941  lmimid  28951  hypcgrlem1  28956  hypcgrlem2  28957  trgcopyeulem  28962  f1otrg  29028  eengtrkg  29144  shuni  31460  5oalem1  31814  5oalem2  31815  5oalem4  31817  5oalem5  31818  3oalem2  31823  pjclem4  32359  pj3si  32367  ccatf1  33088  xrge0tsmsd  33214  wrdpmtrlast  33234  idlinsubrg  33578  ssdifidlprm  33606  qsdrngilem  33643  qsdrngi  33644  pidufd  33700  exsslsb  33855  lindsunlem  33882  lbsdiflsp0  33884  dimkerim  33885  irngss  33945  cmpcref  34108  cmppcmp  34116  dispcmp  34117  zarcmplem  34139  prsdm  34172  prsrn  34173  pnfneige0  34209  qqhucn  34250  rrhqima  34272  gsumesum  34317  esumcst  34321  esum2d  34351  sigainb  34394  inelpisys  34412  dynkin  34425  eulerpartlemgh  34636  eulerpartlemgs2  34638  eulerpartlemn  34639  sseqmw  34649  sseqf  34650  sseqp1  34653  fibp1  34659  bnj1379  35086  bnj1177  35262  cnllysconn  35556  rellysconn  35562  cvmsss2  35585  cvmcov2  35586  cvmopnlem  35589  mclsind  35881  weiunfr  36788  poimirlem30  38110  blbnd  38247  ssbnd  38248  heiborlem1  38271  heiborlem8  38278  heibor  38281  mndomgmid  38331  pmodlem1  40431  pclfinN  40485  mapdunirnN  42235  hdmaprnlem9N  42442  mhpind  43137  elrfi  43236  elrfirn  43237  fnwe2lem2  43589  dfac11  43600  kelac1  43601  kelac2lem  43602  dfac21  43604  islssfgi  43610  filnm  43628  lpirlnr  43655  hbtlem6  43667  hbt  43668  iocinico  43750  restuni3  45657  disjinfi  45731  iooabslt  46036  iocopn  46057  icoopn  46062  uzinico  46096  limciccioolb  46158  limcicciooub  46172  islpcn  46174  limcresioolb  46178  limcleqr  46179  limsuppnfdlem  46236  limsupresxr  46301  liminfresxr  46302  liminfvalxr  46318  liminflelimsupuz  46320  cnrefiisplem  46364  ioccncflimc  46420  icccncfext  46422  icocncflimc  46424  cncfiooicclem1  46428  itgiccshift  46515  itgperiod  46516  itgsbtaddcnst  46517  stoweidlem57  46592  fourierdlem20  46662  fourierdlem32  46674  fourierdlem33  46675  fourierdlem48  46689  fourierdlem49  46690  fourierdlem62  46703  fourierdlem71  46712  fouriersw  46766  qndenserrnbllem  46829  qndenserrn  46834  salgencntex  46878  fsumlesge0  46912  sge0tsms  46915  sge0cl  46916  sge0f1o  46917  sge0sup  46926  sge0resplit  46941  sge0iunmptlemre  46950  sge0fodjrnlem  46951  sge0rpcpnf  46956  sge0xaddlem1  46968  ovolval4lem2  47185  sssmf  47273  smflimlem3  47308  smfsuplem1  47346  fcores  47622  prproropf1olem2  48071  iinfconstbaslem  49647  ffthoppf  49747  uobeqw  49801  uobeq  49802  swapfiso  49867  swapciso  49868  fucoppcffth  49993  thincciso  50035  thinccisod  50036  termcterm  50095  termcterm2  50096  termcterm3  50097  termcciso  50098  termc2  50100  diagciso  50121  diagcic  50122  uobeqterm  50128