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

Theorem elind 4168
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 4166 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 583 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cin 3932
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1787  ax-4 1801  ax-5 1902  ax-6 1961  ax-7 2006  ax-8 2107  ax-9 2115  ax-10 2136  ax-11 2151  ax-12 2167  ax-ext 2790
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 842  df-tru 1531  df-ex 1772  df-nf 1776  df-sb 2061  df-clab 2797  df-cleq 2811  df-clel 2890  df-nfc 2960  df-v 3494  df-in 3940
This theorem is referenced by:  fvelimad  6725  fnfvimad  6987  tfrlem5  8005  uniinqs  8366  unifpw  8815  f1opwfi  8816  fissuni  8817  fipreima  8818  elfir  8867  inelfi  8870  cantnfcl  9118  tskwe  9367  infpwfidom  9442  infpwfien  9476  ackbij2lem1  9629  ackbij1lem3  9632  ackbij1lem4  9633  ackbij1lem6  9635  ackbij1lem11  9640  fin23lem24  9732  isfin1-3  9796  fpwwe2lem12  10051  fpwwe  10056  canthnumlem  10058  fz1isolem  13807  isprm7  16040  setsstruct2  16509  strfv2d  16517  submre  16864  submrc  16887  isacs2  16912  coffth  17194  catcoppccl  17356  catcfuccl  17357  catcxpccl  17445  isdrs2  17537  fpwipodrs  17762  insubm  17971  sylow2a  18673  lsmmod  18730  lsmdisj  18736  lsmdisj2  18737  subgdisj1  18746  frgpnabllem1  18922  dmdprdd  19050  dprdfeq0  19073  dprdres  19079  dprddisj2  19090  dprd2da  19093  dmdprdsplit2lem  19096  ablfacrp  19117  pgpfac1lem3a  19127  pgpfac1lem3  19128  pgpfaclem1  19132  cntzsdrg  19510  aspval  20030  mplind  20210  zringlpirlem1  20559  zringlpirlem3  20561  pmatcoe1fsupp  21237  baspartn  21490  bastg  21502  clsval2  21586  isopn3  21602  restbas  21694  lmss  21834  cmpcovf  21927  discmp  21934  cmpsublem  21935  cmpsub  21936  isconn2  21950  connclo  21951  llynlly  22013  restnlly  22018  restlly  22019  islly2  22020  llyrest  22021  nllyrest  22022  llyidm  22024  nllyidm  22025  hausllycmp  22030  cldllycmp  22031  lly1stc  22032  dislly  22033  llycmpkgen2  22086  1stckgenlem  22089  txlly  22172  txnlly  22173  txtube  22176  txcmplem1  22177  txcmplem2  22178  xkococnlem  22195  basqtop  22247  tgqtop  22248  infil  22399  fmfnfmlem4  22493  hauspwpwf1  22523  tgpconncompss  22649  ustfilxp  22748  metrest  23061  tgioo  23331  zdis  23351  icccmplem1  23357  icccmplem2  23358  reconnlem2  23362  xrge0tsms  23369  cnheibor  23486  cnllycmp  23487  ncvs1  23688  cphsqrtcl  23715  cmetcaulem  23818  ovollb2lem  24016  ovolctb  24018  ovolshftlem1  24037  ovolscalem1  24041  ovolicc1  24044  ioombl1lem1  24086  ioorf  24101  ioorcl  24105  dyadf  24119  vitalilem2  24137  vitali  24141  i1faddlem  24221  i1fmullem  24222  dvres2lem  24435  dvaddbr  24462  dvmulbr  24463  lhop1lem  24537  lhop  24540  dvcnvrelem2  24542  ig1peu  24692  tayl0  24877  rlimcnp2  25471  xrlimcnp  25473  ppisval  25608  ppisval2  25609  ppinprm  25656  chtnprm  25658  2sqlem7  25927  chebbnd1lem1  25972  footexALT  26431  footexlem2  26433  foot  26435  footne  26436  perprag  26439  colperpexlem3  26445  mideulem2  26447  lnopp2hpgb  26476  colopp  26482  lmieu  26497  lmimid  26507  hypcgrlem1  26512  hypcgrlem2  26513  trgcopyeulem  26518  f1otrg  26584  eengtrkg  26699  shuni  29004  5oalem1  29358  5oalem2  29359  5oalem4  29361  5oalem5  29362  3oalem2  29367  pjclem4  29903  pj3si  29911  ccatf1  30552  xrge0tsmsd  30619  lindsunlem  30919  lbsdiflsp0  30921  dimkerim  30922  cmpcref  31013  cmppcmp  31021  dispcmp  31022  prsdm  31056  prsrn  31057  pnfneige0  31093  qqhucn  31132  rrhqima  31154  gsumesum  31217  esumcst  31221  esum2d  31251  sigainb  31294  inelpisys  31312  dynkin  31325  eulerpartlemgh  31535  eulerpartlemgs2  31537  eulerpartlemn  31538  sseqmw  31548  sseqf  31549  sseqp1  31552  fibp1  31558  bnj1379  32001  bnj1177  32175  cnllysconn  32389  rellysconn  32395  cvmsss2  32418  cvmcov2  32419  cvmopnlem  32422  mclsind  32714  frrlem15  33039  poimirlem30  34803  blbnd  34946  ssbnd  34947  heiborlem1  34970  heiborlem8  34977  heibor  34980  mndomgmid  35030  pmodlem1  36862  pclfinN  36916  mapdunirnN  38666  hdmaprnlem9N  38873  elrfi  39169  elrfirn  39170  fnwe2lem2  39529  dfac11  39540  kelac1  39541  kelac2lem  39542  dfac21  39544  islssfgi  39550  filnm  39568  lpirlnr  39595  hbtlem6  39607  hbt  39608  iocinico  39696  restuni3  41261  disjinfi  41330  fvelima2  41408  iooabslt  41650  iocopn  41672  icoopn  41677  uzinico  41712  limciccioolb  41778  limcicciooub  41794  islpcn  41796  limcresioolb  41800  limcleqr  41801  limsuppnfdlem  41858  limsupresxr  41923  liminfresxr  41924  liminfvalxr  41940  liminflelimsupuz  41942  cnrefiisplem  41986  ioccncflimc  42044  icccncfext  42046  icocncflimc  42048  cncfiooicclem1  42052  itgiccshift  42141  itgperiod  42142  itgsbtaddcnst  42143  stoweidlem57  42219  fourierdlem20  42289  fourierdlem32  42301  fourierdlem33  42302  fourierdlem48  42316  fourierdlem49  42317  fourierdlem62  42330  fourierdlem71  42339  fouriersw  42393  qndenserrnbllem  42456  qndenserrn  42461  salgencntex  42503  fsumlesge0  42536  sge0tsms  42539  sge0cl  42540  sge0f1o  42541  sge0sup  42550  sge0resplit  42565  sge0iunmptlemre  42574  sge0fodjrnlem  42575  sge0rpcpnf  42580  sge0xaddlem1  42592  ovolval4lem2  42809  sssmf  42892  smflimlem3  42926  smfsuplem1  42962  prproropf1olem2  43543  zrinitorngc  44199  zrtermorngc  44200  zrzeroorngc  44201  irinitoringc  44268  zrtermoringc  44269  zrninitoringc  44270  nzerooringczr  44271
  Copyright terms: Public domain W3C validator