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

Theorem elind 4170
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 4168 . 2 (𝑋 ∈ (𝐴𝐵) ↔ (𝑋𝐴𝑋𝐵))
41, 2, 3sylanbrc 583 1 (𝜑𝑋 ∈ (𝐴𝐵))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wcel 2105  cin 3934
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 2793
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 2800  df-cleq 2814  df-clel 2893  df-nfc 2963  df-v 3497  df-in 3942
This theorem is referenced by:  fvelimad  6726  fnfvimad  6987  tfrlem5  8007  uniinqs  8367  unifpw  8816  f1opwfi  8817  fissuni  8818  fipreima  8819  elfir  8868  inelfi  8871  cantnfcl  9119  tskwe  9368  infpwfidom  9443  infpwfien  9477  ackbij2lem1  9630  ackbij1lem3  9633  ackbij1lem4  9634  ackbij1lem6  9636  ackbij1lem11  9641  fin23lem24  9733  isfin1-3  9797  fpwwe2lem12  10052  fpwwe  10057  canthnumlem  10059  fz1isolem  13809  isprm7  16042  setsstruct2  16511  strfv2d  16519  submre  16866  submrc  16889  isacs2  16914  coffth  17196  catcoppccl  17358  catcfuccl  17359  catcxpccl  17447  isdrs2  17539  fpwipodrs  17764  insubm  17973  sylow2a  18675  lsmmod  18732  lsmdisj  18738  lsmdisj2  18739  subgdisj1  18748  frgpnabllem1  18924  dmdprdd  19052  dprdfeq0  19075  dprdres  19081  dprddisj2  19092  dprd2da  19095  dmdprdsplit2lem  19098  ablfacrp  19119  pgpfac1lem3a  19129  pgpfac1lem3  19130  pgpfaclem1  19134  cntzsdrg  19512  aspval  20032  mplind  20212  zringlpirlem1  20561  zringlpirlem3  20563  pmatcoe1fsupp  21239  baspartn  21492  bastg  21504  clsval2  21588  isopn3  21604  restbas  21696  lmss  21836  cmpcovf  21929  discmp  21936  cmpsublem  21937  cmpsub  21938  isconn2  21952  connclo  21953  llynlly  22015  restnlly  22020  restlly  22021  islly2  22022  llyrest  22023  nllyrest  22024  llyidm  22026  nllyidm  22027  hausllycmp  22032  cldllycmp  22033  lly1stc  22034  dislly  22035  llycmpkgen2  22088  1stckgenlem  22091  txlly  22174  txnlly  22175  txtube  22178  txcmplem1  22179  txcmplem2  22180  xkococnlem  22197  basqtop  22249  tgqtop  22250  infil  22401  fmfnfmlem4  22495  hauspwpwf1  22525  tgpconncompss  22651  ustfilxp  22750  metrest  23063  tgioo  23333  zdis  23353  icccmplem1  23359  icccmplem2  23360  reconnlem2  23364  xrge0tsms  23371  cnheibor  23488  cnllycmp  23489  ncvs1  23690  cphsqrtcl  23717  cmetcaulem  23820  ovollb2lem  24018  ovolctb  24020  ovolshftlem1  24039  ovolscalem1  24043  ovolicc1  24046  ioombl1lem1  24088  ioorf  24103  ioorcl  24107  dyadf  24121  vitalilem2  24139  vitali  24143  i1faddlem  24223  i1fmullem  24224  dvres2lem  24437  dvaddbr  24464  dvmulbr  24465  lhop1lem  24539  lhop  24542  dvcnvrelem2  24544  ig1peu  24694  tayl0  24879  rlimcnp2  25472  xrlimcnp  25474  ppisval  25609  ppisval2  25610  ppinprm  25657  chtnprm  25659  2sqlem7  25928  chebbnd1lem1  25973  footexALT  26432  footexlem2  26434  foot  26436  footne  26437  perprag  26440  colperpexlem3  26446  mideulem2  26448  lnopp2hpgb  26477  colopp  26483  lmieu  26498  lmimid  26508  hypcgrlem1  26513  hypcgrlem2  26514  trgcopyeulem  26519  f1otrg  26585  eengtrkg  26700  shuni  29005  5oalem1  29359  5oalem2  29360  5oalem4  29362  5oalem5  29363  3oalem2  29368  pjclem4  29904  pj3si  29912  ccatf1  30553  xrge0tsmsd  30620  lindsunlem  30920  lbsdiflsp0  30922  dimkerim  30923  cmpcref  31014  cmppcmp  31022  dispcmp  31023  prsdm  31057  prsrn  31058  pnfneige0  31094  qqhucn  31133  rrhqima  31155  gsumesum  31218  esumcst  31222  esum2d  31252  sigainb  31295  inelpisys  31313  dynkin  31326  eulerpartlemgh  31536  eulerpartlemgs2  31538  eulerpartlemn  31539  sseqmw  31549  sseqf  31550  sseqp1  31553  fibp1  31559  bnj1379  32002  bnj1177  32176  cnllysconn  32390  rellysconn  32396  cvmsss2  32419  cvmcov2  32420  cvmopnlem  32423  mclsind  32715  frrlem15  33040  poimirlem30  34804  blbnd  34948  ssbnd  34949  heiborlem1  34972  heiborlem8  34979  heibor  34982  mndomgmid  35032  pmodlem1  36864  pclfinN  36918  mapdunirnN  38668  hdmaprnlem9N  38875  elrfi  39171  elrfirn  39172  fnwe2lem2  39531  dfac11  39542  kelac1  39543  kelac2lem  39544  dfac21  39546  islssfgi  39552  filnm  39570  lpirlnr  39597  hbtlem6  39609  hbt  39610  iocinico  39698  restuni3  41265  disjinfi  41334  fvelima2  41412  iooabslt  41654  iocopn  41676  icoopn  41681  uzinico  41716  limciccioolb  41782  limcicciooub  41798  islpcn  41800  limcresioolb  41804  limcleqr  41805  limsuppnfdlem  41862  limsupresxr  41927  liminfresxr  41928  liminfvalxr  41944  liminflelimsupuz  41946  cnrefiisplem  41990  ioccncflimc  42048  icccncfext  42050  icocncflimc  42052  cncfiooicclem1  42056  itgiccshift  42145  itgperiod  42146  itgsbtaddcnst  42147  stoweidlem57  42223  fourierdlem20  42293  fourierdlem32  42305  fourierdlem33  42306  fourierdlem48  42320  fourierdlem49  42321  fourierdlem62  42334  fourierdlem71  42343  fouriersw  42397  qndenserrnbllem  42460  qndenserrn  42465  salgencntex  42507  fsumlesge0  42540  sge0tsms  42543  sge0cl  42544  sge0f1o  42545  sge0sup  42554  sge0resplit  42569  sge0iunmptlemre  42578  sge0fodjrnlem  42579  sge0rpcpnf  42584  sge0xaddlem1  42596  ovolval4lem2  42813  sssmf  42896  smflimlem3  42930  smfsuplem1  42966  prproropf1olem2  43513  zrinitorngc  44169  zrtermorngc  44170  zrzeroorngc  44171  irinitoringc  44238  zrtermoringc  44239  zrninitoringc  44240  nzerooringczr  44241
  Copyright terms: Public domain W3C validator