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

Theorem elind 3760
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 3758 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 695 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 1977  cin 3539
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1713  ax-4 1728  ax-5 1827  ax-6 1875  ax-7 1922  ax-10 2006  ax-11 2021  ax-12 2034  ax-13 2234  ax-ext 2590
This theorem depends on definitions:  df-bi 196  df-or 384  df-an 385  df-tru 1478  df-ex 1696  df-nf 1701  df-sb 1868  df-clab 2597  df-cleq 2603  df-clel 2606  df-nfc 2740  df-v 3175  df-in 3547
This theorem is referenced by:  tfrlem5  7363  uniinqs  7714  unifpw  8152  f1opwfi  8153  fissuni  8154  fipreima  8155  elfir  8204  inelfi  8207  cantnfcl  8447  tskwe  8659  infpwfidom  8734  infpwfien  8768  ackbij2lem1  8924  ackbij1lem3  8927  ackbij1lem4  8928  ackbij1lem6  8930  ackbij1lem11  8935  fin23lem24  9027  isfin1-3  9091  fpwwe2lem12  9342  fpwwe  9347  canthnumlem  9349  fz1isolem  13102  isprm7  15258  strfv2d  15733  submre  16088  submrc  16111  isacs2  16137  coffth  16419  catcoppccl  16581  catcfuccl  16582  catcxpccl  16670  isdrs2  16762  fpwipodrs  16987  sylow2a  17857  lsmmod  17911  lsmdisj  17917  lsmdisj2  17918  subgdisj1  17927  frgpnabllem1  18099  dmdprdd  18221  dprdfeq0  18244  dprdres  18250  dprddisj2  18261  dprd2da  18264  dmdprdsplit2lem  18267  ablfacrp  18288  pgpfac1lem3a  18298  pgpfac1lem3  18299  pgpfaclem1  18303  aspval  19149  mplind  19323  zringlpirlem1  19651  zringlpirlem3  19653  pmatcoe1fsupp  20325  baspartn  20569  bastg  20581  clsval2  20664  isopn3  20680  restbas  20772  lmss  20912  cmpcovf  21004  discmp  21011  cmpsublem  21012  cmpsub  21013  iscon2  21027  conclo  21028  llynlly  21090  restnlly  21095  restlly  21096  islly2  21097  llyrest  21098  nllyrest  21099  llyidm  21101  nllyidm  21102  hausllycmp  21107  cldllycmp  21108  lly1stc  21109  dislly  21110  llycmpkgen2  21163  1stckgenlem  21166  txlly  21249  txnlly  21250  txtube  21253  txcmplem1  21254  txcmplem2  21255  xkococnlem  21272  basqtop  21324  tgqtop  21325  infil  21477  fmfnfmlem4  21571  hauspwpwf1  21601  tgpconcompss  21727  ustfilxp  21826  metrest  22139  tgioo  22407  zdis  22427  icccmplem1  22433  icccmplem2  22434  reconnlem2  22438  xrge0tsms  22445  cnheibor  22562  cnllycmp  22563  ncvs1  22765  cphsqrtcl  22792  cmetcaulem  22894  ovollb2lem  23063  ovolctb  23065  ovolshftlem1  23084  ovolscalem1  23088  ovolicc1  23091  ioombl1lem1  23133  ioorf  23147  ioorcl  23151  dyadf  23165  vitalilem2  23184  vitali  23188  i1faddlem  23266  dvres2lem  23480  dvaddbr  23507  dvmulbr  23508  lhop1lem  23580  lhop  23583  dvcnvrelem2  23585  ig1peu  23735  tayl0  23920  rlimcnp2  24493  xrlimcnp  24495  ppisval  24630  ppisval2  24631  ppinprm  24678  chtnprm  24680  2sqlem7  24949  chebbnd1lem1  24958  footex  25413  foot  25414  footne  25415  perprag  25418  colperpexlem3  25424  mideulem2  25426  lnopp2hpgb  25455  colopp  25461  lmieu  25476  lmimid  25486  hypcgrlem1  25491  hypcgrlem2  25492  trgcopyeulem  25497  f1otrg  25551  eengtrkg  25665  shuni  27543  5oalem1  27897  5oalem2  27898  5oalem4  27900  5oalem5  27901  3oalem2  27906  pjclem4  28442  pj3si  28450  xrge0tsmsd  29116  cmpcref  29245  cmppcmp  29253  dispcmp  29254  prsdm  29288  prsrn  29289  pnfneige0  29325  qqhucn  29364  rrhqima  29386  gsumesum  29448  esumcst  29452  esum2d  29482  sigainb  29526  inelpisys  29544  dynkin  29557  eulerpartlemgh  29767  eulerpartlemgs2  29769  eulerpartlemn  29770  sseqmw  29780  sseqf  29781  sseqp1  29784  fibp1  29790  bnj1379  30155  bnj1177  30328  cnllyscon  30481  rellyscon  30487  cvmsss2  30510  cvmcov2  30511  cvmopnlem  30514  mclsind  30721  poimirlem30  32609  blbnd  32756  ssbnd  32757  heiborlem1  32780  heiborlem8  32787  heibor  32790  mndomgmid  32840  pmodlem1  34150  pclfinN  34204  mapdunirnN  35957  hdmaprnlem9N  36167  elrfi  36275  elrfirn  36276  fnwe2lem2  36639  dfac11  36650  kelac1  36651  kelac2lem  36652  dfac21  36654  islssfgi  36660  filnm  36678  lpirlnr  36706  hbtlem6  36718  hbt  36719  cntzsdrg  36791  iocinico  36816  restuni3  38333  disjinfi  38375  iooabslt  38568  iocopn  38593  icoopn  38598  limciccioolb  38688  limcicciooub  38704  islpcn  38706  limcresioolb  38710  limcleqr  38711  ioccncflimc  38771  icccncfext  38773  icocncflimc  38775  cncfiooicclem1  38779  itgiccshift  38872  itgperiod  38873  itgsbtaddcnst  38874  stoweidlem57  38950  fourierdlem20  39020  fourierdlem32  39032  fourierdlem33  39033  fourierdlem48  39047  fourierdlem49  39048  fourierdlem62  39061  fourierdlem71  39070  fouriersw  39124  qndenserrnbllem  39190  qndenserrn  39195  salgencntex  39237  fsumlesge0  39270  sge0tsms  39273  sge0cl  39274  sge0f1o  39275  sge0sup  39284  sge0resplit  39299  sge0iunmptlemre  39308  sge0fodjrnlem  39309  sge0rpcpnf  39314  sge0xaddlem1  39326  ovolval4lem2  39540  sssmf  39625  smflimlem3  39659  1wlkres  40879  zrinitorngc  41792  zrtermorngc  41793  zrzeroorngc  41794  irinitoringc  41861  zrtermoringc  41862  zrninitoringc  41863  nzerooringczr  41864
  Copyright terms: Public domain W3C validator