MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elind Structured version   Visualization version   GIF version

Theorem elind 3947
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
StepHypRef Expression
1 elind.1 . 2 (𝜑𝑋𝐴)
2 elind.2 . 2 (𝜑𝑋𝐵)
3 elin 3945 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 564 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2144  cin 3720
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1869  ax-4 1884  ax-5 1990  ax-6 2056  ax-7 2092  ax-9 2153  ax-10 2173  ax-11 2189  ax-12 2202  ax-13 2407  ax-ext 2750
This theorem depends on definitions:  df-bi 197  df-an 383  df-or 827  df-tru 1633  df-ex 1852  df-nf 1857  df-sb 2049  df-clab 2757  df-cleq 2763  df-clel 2766  df-nfc 2901  df-v 3351  df-in 3728
This theorem is referenced by:  tfrlem5  7628  uniinqs  7978  unifpw  8424  f1opwfi  8425  fissuni  8426  fipreima  8427  elfir  8476  inelfi  8479  cantnfcl  8727  tskwe  8975  infpwfidom  9050  infpwfien  9084  ackbij2lem1  9242  ackbij1lem3  9245  ackbij1lem4  9246  ackbij1lem6  9248  ackbij1lem11  9253  fin23lem24  9345  isfin1-3  9409  fpwwe2lem12  9664  fpwwe  9669  canthnumlem  9671  fz1isolem  13446  isprm7  15626  setsstruct2  16102  strfv2d  16111  submre  16472  submrc  16495  isacs2  16520  coffth  16802  catcoppccl  16964  catcfuccl  16965  catcxpccl  17054  isdrs2  17146  fpwipodrs  17371  sylow2a  18240  lsmmod  18294  lsmdisj  18300  lsmdisj2  18301  subgdisj1  18310  frgpnabllem1  18482  dmdprdd  18605  dprdfeq0  18628  dprdres  18634  dprddisj2  18645  dprd2da  18648  dmdprdsplit2lem  18651  ablfacrp  18672  pgpfac1lem3a  18682  pgpfac1lem3  18683  pgpfaclem1  18687  aspval  19542  mplind  19716  zringlpirlem1  20046  zringlpirlem3  20048  pmatcoe1fsupp  20725  baspartn  20978  bastg  20990  clsval2  21074  isopn3  21090  restbas  21182  lmss  21322  cmpcovf  21414  discmp  21421  cmpsublem  21422  cmpsub  21423  isconn2  21437  connclo  21438  llynlly  21500  restnlly  21505  restlly  21506  islly2  21507  llyrest  21508  nllyrest  21509  llyidm  21511  nllyidm  21512  hausllycmp  21517  cldllycmp  21518  lly1stc  21519  dislly  21520  llycmpkgen2  21573  1stckgenlem  21576  txlly  21659  txnlly  21660  txtube  21663  txcmplem1  21664  txcmplem2  21665  xkococnlem  21682  basqtop  21734  tgqtop  21735  infil  21886  fmfnfmlem4  21980  hauspwpwf1  22010  tgpconncompss  22136  ustfilxp  22235  metrest  22548  tgioo  22818  zdis  22838  icccmplem1  22844  icccmplem2  22845  reconnlem2  22849  xrge0tsms  22856  cnheibor  22973  cnllycmp  22974  ncvs1  23175  cphsqrtcl  23202  cmetcaulem  23304  ovollb2lem  23475  ovolctb  23477  ovolshftlem1  23496  ovolscalem1  23500  ovolicc1  23503  ioombl1lem1  23545  ioorf  23560  ioorcl  23564  dyadf  23578  vitalilem2  23596  vitali  23600  i1faddlem  23679  dvres2lem  23893  dvaddbr  23920  dvmulbr  23921  lhop1lem  23995  lhop  23998  dvcnvrelem2  24000  ig1peu  24150  tayl0  24335  rlimcnp2  24913  xrlimcnp  24915  ppisval  25050  ppisval2  25051  ppinprm  25098  chtnprm  25100  2sqlem7  25369  chebbnd1lem1  25378  footex  25833  foot  25834  footne  25835  perprag  25838  colperpexlem3  25844  mideulem2  25846  lnopp2hpgb  25875  colopp  25881  lmieu  25896  lmimid  25906  hypcgrlem1  25911  hypcgrlem2  25912  trgcopyeulem  25917  f1otrg  25971  eengtrkg  26085  wlkres  26801  shuni  28493  5oalem1  28847  5oalem2  28848  5oalem4  28850  5oalem5  28851  3oalem2  28856  pjclem4  29392  pj3si  29400  xrge0tsmsd  30119  cmpcref  30251  cmppcmp  30259  dispcmp  30260  prsdm  30294  prsrn  30295  pnfneige0  30331  qqhucn  30370  rrhqima  30392  gsumesum  30455  esumcst  30459  esum2d  30489  sigainb  30533  inelpisys  30551  dynkin  30564  eulerpartlemgh  30774  eulerpartlemgs2  30776  eulerpartlemn  30777  sseqmw  30787  sseqf  30788  sseqp1  30791  fibp1  30797  bnj1379  31233  bnj1177  31406  cnllysconn  31559  rellysconn  31565  cvmsss2  31588  cvmcov2  31589  cvmopnlem  31592  mclsind  31799  poimirlem30  33765  blbnd  33911  ssbnd  33912  heiborlem1  33935  heiborlem8  33942  heibor  33945  mndomgmid  33995  pmodlem1  35647  pclfinN  35701  mapdunirnN  37453  hdmaprnlem9N  37660  elrfi  37776  elrfirn  37777  fnwe2lem2  38140  dfac11  38151  kelac1  38152  kelac2lem  38153  dfac21  38155  islssfgi  38161  filnm  38179  lpirlnr  38206  hbtlem6  38218  hbt  38219  cntzsdrg  38291  iocinico  38316  restuni3  39816  disjinfi  39894  fvelimad  39970  fnfvimad  39971  fvelima2  39987  fnfvima2  39990  iooabslt  40236  iocopn  40259  icoopn  40264  uzinico  40299  limciccioolb  40365  limcicciooub  40381  islpcn  40383  limcresioolb  40387  limcleqr  40388  limsuppnfdlem  40445  limsupresxr  40510  liminfresxr  40511  liminfvalxr  40527  liminflelimsupuz  40529  cnrefiisplem  40567  ioccncflimc  40610  icccncfext  40612  icocncflimc  40614  cncfiooicclem1  40618  itgiccshift  40707  itgperiod  40708  itgsbtaddcnst  40709  stoweidlem57  40785  fourierdlem20  40855  fourierdlem32  40867  fourierdlem33  40868  fourierdlem48  40882  fourierdlem49  40883  fourierdlem62  40896  fourierdlem71  40905  fouriersw  40959  qndenserrnbllem  41025  qndenserrn  41030  salgencntex  41072  fsumlesge0  41105  sge0tsms  41108  sge0cl  41109  sge0f1o  41110  sge0sup  41119  sge0resplit  41134  sge0iunmptlemre  41143  sge0fodjrnlem  41144  sge0rpcpnf  41149  sge0xaddlem1  41161  ovolval4lem2  41378  sssmf  41461  smflimlem3  41495  smfsuplem1  41531  zrinitorngc  42518  zrtermorngc  42519  zrzeroorngc  42520  irinitoringc  42587  zrtermoringc  42588  zrninitoringc  42589  nzerooringczr  42590
  Copyright terms: Public domain W3C validator