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

Theorem elind 3994
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 3992 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 579 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2157  cin 3766
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1891  ax-4 1905  ax-5 2006  ax-6 2072  ax-7 2107  ax-9 2166  ax-10 2185  ax-11 2200  ax-12 2213  ax-ext 2775
This theorem depends on definitions:  df-bi 199  df-an 386  df-or 875  df-tru 1657  df-ex 1876  df-nf 1880  df-sb 2065  df-clab 2784  df-cleq 2790  df-clel 2793  df-nfc 2928  df-v 3385  df-in 3774
This theorem is referenced by:  tfrlem5  7713  uniinqs  8063  unifpw  8509  f1opwfi  8510  fissuni  8511  fipreima  8512  elfir  8561  inelfi  8564  cantnfcl  8812  tskwe  9060  infpwfidom  9135  infpwfien  9169  ackbij2lem1  9327  ackbij1lem3  9330  ackbij1lem4  9331  ackbij1lem6  9333  ackbij1lem11  9338  fin23lem24  9430  isfin1-3  9494  fpwwe2lem12  9749  fpwwe  9754  canthnumlem  9756  fz1isolem  13490  isprm7  15749  setsstruct2  16218  strfv2d  16226  submre  16576  submrc  16599  isacs2  16624  coffth  16906  catcoppccl  17068  catcfuccl  17069  catcxpccl  17158  isdrs2  17250  fpwipodrs  17475  sylow2a  18343  lsmmod  18397  lsmdisj  18403  lsmdisj2  18404  subgdisj1  18413  frgpnabllem1  18587  dmdprdd  18710  dprdfeq0  18733  dprdres  18739  dprddisj2  18750  dprd2da  18753  dmdprdsplit2lem  18756  ablfacrp  18777  pgpfac1lem3a  18787  pgpfac1lem3  18788  pgpfaclem1  18792  aspval  19647  mplind  19820  zringlpirlem1  20150  zringlpirlem3  20152  pmatcoe1fsupp  20830  baspartn  21083  bastg  21095  clsval2  21179  isopn3  21195  restbas  21287  lmss  21427  cmpcovf  21519  discmp  21526  cmpsublem  21527  cmpsub  21528  isconn2  21542  connclo  21543  llynlly  21605  restnlly  21610  restlly  21611  islly2  21612  llyrest  21613  nllyrest  21614  llyidm  21616  nllyidm  21617  hausllycmp  21622  cldllycmp  21623  lly1stc  21624  dislly  21625  llycmpkgen2  21678  1stckgenlem  21681  txlly  21764  txnlly  21765  txtube  21768  txcmplem1  21769  txcmplem2  21770  xkococnlem  21787  basqtop  21839  tgqtop  21840  infil  21991  fmfnfmlem4  22085  hauspwpwf1  22115  tgpconncompss  22241  ustfilxp  22340  metrest  22653  tgioo  22923  zdis  22943  icccmplem1  22949  icccmplem2  22950  reconnlem2  22954  xrge0tsms  22961  cnheibor  23078  cnllycmp  23079  ncvs1  23280  cphsqrtcl  23307  cmetcaulem  23410  ovollb2lem  23592  ovolctb  23594  ovolshftlem1  23613  ovolscalem1  23617  ovolicc1  23620  ioombl1lem1  23662  ioorf  23677  ioorcl  23681  dyadf  23695  vitalilem2  23713  vitali  23717  i1faddlem  23797  dvres2lem  24011  dvaddbr  24038  dvmulbr  24039  lhop1lem  24113  lhop  24116  dvcnvrelem2  24118  ig1peu  24268  tayl0  24453  rlimcnp2  25041  xrlimcnp  25043  ppisval  25178  ppisval2  25179  ppinprm  25226  chtnprm  25228  2sqlem7  25497  chebbnd1lem1  25506  footex  25961  foot  25962  footne  25963  perprag  25966  colperpexlem3  25972  mideulem2  25974  lnopp2hpgb  26003  colopp  26009  lmieu  26024  lmimid  26034  hypcgrlem1  26039  hypcgrlem2  26040  trgcopyeulem  26045  f1otrg  26099  eengtrkg  26213  wlkresOLD  26914  shuni  28675  5oalem1  29029  5oalem2  29030  5oalem4  29032  5oalem5  29033  3oalem2  29038  pjclem4  29574  pj3si  29582  xrge0tsmsd  30292  cmpcref  30424  cmppcmp  30432  dispcmp  30433  prsdm  30467  prsrn  30468  pnfneige0  30504  qqhucn  30543  rrhqima  30565  gsumesum  30628  esumcst  30632  esum2d  30662  sigainb  30706  inelpisys  30724  dynkin  30737  eulerpartlemgh  30947  eulerpartlemgs2  30949  eulerpartlemn  30950  sseqmw  30961  sseqf  30962  sseqp1  30965  fibp1  30971  bnj1379  31409  bnj1177  31582  cnllysconn  31735  rellysconn  31741  cvmsss2  31764  cvmcov2  31765  cvmopnlem  31768  mclsind  31975  poimirlem30  33919  blbnd  34064  ssbnd  34065  heiborlem1  34088  heiborlem8  34095  heibor  34098  mndomgmid  34148  pmodlem1  35858  pclfinN  35912  mapdunirnN  37662  hdmaprnlem9N  37869  elrfi  38030  elrfirn  38031  fnwe2lem2  38393  dfac11  38404  kelac1  38405  kelac2lem  38406  dfac21  38408  islssfgi  38414  filnm  38432  lpirlnr  38459  hbtlem6  38471  hbt  38472  cntzsdrg  38544  iocinico  38568  restuni3  40046  disjinfi  40121  fvelimad  40193  fnfvimad  40194  fvelima2  40209  fnfvima2  40212  iooabslt  40456  iocopn  40478  icoopn  40483  uzinico  40518  limciccioolb  40584  limcicciooub  40600  islpcn  40602  limcresioolb  40606  limcleqr  40607  limsuppnfdlem  40664  limsupresxr  40729  liminfresxr  40730  liminfvalxr  40746  liminflelimsupuz  40748  cnrefiisplem  40786  ioccncflimc  40829  icccncfext  40831  icocncflimc  40833  cncfiooicclem1  40837  itgiccshift  40926  itgperiod  40927  itgsbtaddcnst  40928  stoweidlem57  41004  fourierdlem20  41074  fourierdlem32  41086  fourierdlem33  41087  fourierdlem48  41101  fourierdlem49  41102  fourierdlem62  41115  fourierdlem71  41124  fouriersw  41178  qndenserrnbllem  41244  qndenserrn  41249  salgencntex  41291  fsumlesge0  41324  sge0tsms  41327  sge0cl  41328  sge0f1o  41329  sge0sup  41338  sge0resplit  41353  sge0iunmptlemre  41362  sge0fodjrnlem  41363  sge0rpcpnf  41368  sge0xaddlem1  41380  ovolval4lem2  41597  sssmf  41680  smflimlem3  41714  smfsuplem1  41750  zrinitorngc  42786  zrtermorngc  42787  zrzeroorngc  42788  irinitoringc  42855  zrtermoringc  42856  zrninitoringc  42857  nzerooringczr  42858
  Copyright terms: Public domain W3C validator