MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  elin Unicode version

Theorem elin 3686
Description: Expansion of membership in an intersection of two classes. Theorem 12 of [Suppes] p. 25. (Contributed by NM, 29-Apr-1994.)
Assertion
Ref Expression
elin

Proof of Theorem elin
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 elex 3118 . 2
2 elex 3118 . . 3
32adantl 466 . 2
4 eleq1 2529 . . . 4
5 eleq1 2529 . . . 4
64, 5anbi12d 710 . . 3
7 df-in 3482 . . 3
86, 7elab2g 3248 . 2
91, 3, 8pm5.21nii 353 1
Colors of variables: wff setvar class
Syntax hints:  <->wb 184  /\wa 369  =wceq 1395  e.wcel 1818   cvv 3109  i^icin 3474
This theorem is referenced by:  elind  3687  elin2  3688  elin3  3689  incom  3690  ineqri  3691  ineq1  3692  inass  3707  inss1  3717  ssin  3719  ssrin  3722  dfss4  3731  difin  3734  indi  3743  undi  3744  unineq  3747  indifdir  3753  difin2  3759  inrab2  3770  inelcm  3881  difin0ss  3894  inssdif0  3895  inundif  3906  uniin  4269  intun  4319  intpr  4320  elrint  4328  iunin2  4394  iinin2  4400  elriin  4403  disjor  4436  disjiun  4442  brin  4501  trin  4555  inex1  4593  inuni  4614  wefrc  4878  ordtri3or  4915  inopab  5138  inxp  5140  dmin  5215  opelres  5284  eldmeldmressn  5319  intasym  5387  asymref  5388  dminss  5425  imainss  5426  inimasn  5428  ssrnres  5450  cnvresima  5501  dfco2a  5512  2elresin  5697  respreima  6016  fvcofneq  6039  isomin  6233  isoini  6234  offval  6547  ordpwsuc  6650  ressuppss  6938  erdisj  7378  uniinqs  7410  mapval2  7468  ixpin  7514  boxriin  7531  disjen  7694  ssenen  7711  onfin2  7729  elfpw  7842  fiin  7902  inf3lem2  8067  epfrs  8183  cp  8330  bnd2  8332  dfac5lem1  8525  dfac5lem5  8529  dfac5  8530  kmlem3  8553  kmlem14  8564  kmlem15  8565  fin23lem26  8726  isfin1-3  8787  pwxpndom2  9064  ingru  9214  gruina  9217  grur1  9219  axgroth4  9231  grothprim  9233  ixxdisj  11573  icodisj  11674  fzdisj  11741  uzdisj  11780  nn0disj  11820  fzouzdisj  11861  limsupgle  13300  ello12  13339  elo12  13350  lo1resb  13387  rlimresb  13388  o1resb  13389  lo1eq  13391  rlimeq  13392  fsumsplit  13562  sumsplit  13583  fsum2dlem  13585  explecnv  13676  fprod2dlem  13784  bitsmod  14086  saddisjlem  14114  sadadd  14117  sadass  14121  smuval2  14132  smupval  14138  smueqlem  14140  smumul  14143  prmreclem5  14438  prmrec  14440  4sqlem12  14474  vdwmc  14496  acsfn  15056  isdrs2  15568  fpwipodrs  15794  psss  15844  subgacs  16236  nsgacs  16237  resscntz  16369  gsmsymgreq  16457  sylow2a  16639  lsmmod  16693  lsmdisj2  16700  gsumzsplit  16944  gsumzsplitOLD  16945  subgdmdprd  17081  dprdcntz2  17086  dprddisj2  17087  dprddisj2OLD  17088  pgpfac1lem3  17128  isrhm  17370  subsubrg2  17456  lssacs  17613  lspdisj  17771  lspdisjb  17772  isassa  17964  aspid  17979  aspval2  17996  dfprm2  18524  dfprm2OLD  18527  ocvin  18705  unocv  18711  iunocv  18712  obselocv  18759  pmatcoe1fsupp  19202  isbasis2g  19449  tgval2  19457  tgcl  19471  ppttop  19508  epttop  19510  clsval2  19551  ssntr  19559  ntreq0  19578  isclo  19588  restntr  19683  restlp  19684  cnpresti  19789  cnprest  19790  cnprest2  19791  lmss  19799  haust1  19853  nrmsep3  19856  isnrm2  19859  lmmo  19881  fincmp  19893  0cmp  19894  discmp  19898  cmpsublem  19899  cmpsub  19900  uncmp  19903  hauscmplem  19906  bwthOLD  19911  dfcon2  19920  iunconlem  19928  uncon  19930  is1stc2  19943  1stcrest  19954  1stcelcls  19962  llyi  19975  nllyi  19976  subislly  19982  lly1stc  19997  comppfsc  20033  txcnp  20121  txcnmpt  20125  hausdiag  20146  kqcldsat  20234  ptcmpfi  20314  isfbas2  20336  isfil2  20357  fbasfip  20369  elfg  20372  filcon  20384  rnelfmlem  20453  rnelfm  20454  fmfnfmlem2  20456  fmfnfmlem4  20458  fmfnfm  20459  flimrest  20484  hauspwpwf1  20488  fclsrest  20525  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  alexsubALT  20551  ptcmp  20558  istmd  20573  istgp  20576  tsmssubm  20644  tsmssplit  20654  istrg  20666  istdrg  20668  istlm  20687  ustfilxp  20715  utoptop  20737  utop3cls  20754  bldisj  20901  blin  20924  blin2  20932  blres  20934  lpbl  21006  metrest  21027  restmetu  21090  isngp  21116  isnlm  21184  isnmhm  21253  xrtgioo  21311  xrsmopn  21317  icccmplem2  21328  reconnlem2  21332  icoopnst  21439  iocopnst  21440  bndth  21458  iscph  21617  tchcph  21680  cfilfcls  21713  cmetcaulem  21727  cmetss  21753  isbn  21777  cldcss2  21857  hlhil  21858  ovolfcl  21878  ovolicc1  21927  ovolicc2lem2  21929  ovolicc2lem4  21931  ovolicc2lem5  21932  ovolicc2  21933  shftmbl  21949  volfiniun  21957  ioorf  21982  mbfmax  22056  mbfimaopnlem  22062  mbfaddlem  22067  mbfadd  22068  mbfsub  22069  i1faddlem  22100  i1fmullem  22101  i1fres  22112  itg1climres  22121  mbfi1fseqlem4  22125  mbfmul  22133  itg2splitlem  22155  itg2split  22156  itgresr  22185  bddmulibl  22245  ellimc2  22281  ellimc3  22283  limcun  22299  dvreslem  22313  dvne0  22412  itgsubstlem  22449  ig1pval3  22575  aaliou2  22736  aaliou2b  22737  pilem1  22846  rlimcnp2  23296  fsumharmonic  23341  ppisval2  23378  prmorcht  23452  fsumvma2  23489  pclogsum  23490  vmasum  23491  chpchtsum  23494  chpub  23495  chebbnd1lem1  23654  rpvmasum2  23697  tglineineq  24023  frgrancvvdeqlem4  25033  frgrancvvdeqlem7  25036  frgrancvvdeqlemA  25037  frgrancvvdeqlemC  25039  issubgo  25305  isexid2  25327  smgrpismgmOLD  25334  smgrpisass  25335  issmgrpOLD  25336  mndoissmgrpOLD  25341  mndoisexid  25342  ismndo  25345  rngo1cl  25431  minvecolem1  25790  minvecolem4a  25793  minvecolem4b  25794  minvecolem4  25796  h2hcau  25896  axhcompl-zf  25915  hhcmpl  26117  hhcms  26120  ocin  26214  ocnel  26216  shmodsi  26307  pjhthlem2  26310  omlsilem  26320  pjoc1i  26349  spansnm0i  26568  nonbooli  26569  5oalem7  26578  3oalem3  26582  pjssmii  26599  mayete3i  26646  mayete3iOLD  26647  nmcopex  26948  nmcoplb  26949  lncnopbd  26956  nmcfnex  26972  nmcfnlb  26973  riesz4  26983  riesz1  26984  riesz2  26985  cnlnadjlem3  26988  cnlnadjlem5  26990  cnlnadjlem9  26994  cnlnadjeu  26997  rnbra  27026  pjimai  27095  pjclem4a  27117  pj3lem1  27125  jpi  27189  sumdmdii  27334  sumdmdlem  27337  sumdmdlem2  27338  cdjreui  27351  cdj3lem1  27353  disjorf  27440  ofpreima  27507  1stpreima  27524  2ndpreima  27525  iocinioc2  27590  ssnnssfz  27597  isorng  27789  kerunit  27813  crefdf  27851  cmpcref  27853  cmppcmp  27861  pcmplfin  27863  cnre2csqima  27893  ordtconlem1  27906  lmxrge0  27934  isrrext  27981  esum0  28060  esumcst  28071  esumpcvgval  28084  esumcvg  28092  measvuni  28185  eulerpartlemt0  28308  eulerpartlemr  28313  eulerpartlemgf  28318  eulerpartlemgs2  28319  eulerpartlemn  28320  sseqf  28331  fiblem  28337  dfres3  29188  elima4  29209  dfon2lem4  29218  predel  29263  wfrlem5  29347  frrlem5  29391  ellimits  29560  dfom5b  29562  brapply  29588  brcap  29590  dfrdg4  29600  tfrqfree  29601  onsucconi  29902  onintopsscon  29905  onsucsuccmpi  29908  limsucncmpi  29910  onint1  29914  ptrest  30048  mblfinlem2  30052  mbfposadd  30062  itg2gt0cn  30070  dvasin  30103  finminlem  30136  neibastop2lem  30178  neibastop2  30179  neifg  30189  tailfb  30195  inixp  30219  0totbnd  30269  sstotbnd3  30272  heibor1lem  30305  heibor1  30306  heiborlem6  30312  exidresid  30341  isfld2  30402  prtlem14  30615  cmpfiiin  30629  mrefg2  30639  fz1eqin  30702  fnwe2lem2  30997  islmodfg  31015  islssfg2  31017  lnr2i  31065  acsfn1p  31148  subrgacs  31149  sdrgacs  31150  isprm7  31192  radcnvrat  31195  nzin  31223  elinel2  31423  elinel1  31424  iooabslt  31532  iccintsng  31563  lptioo2cn  31651  lptioo1cn  31652  cncfuni  31689  icccncfext  31690  stoweidlem44  31826  fourierdlem42  31931  fourierdlem80  31969  eldmressn  32208  afvres  32257  tpres  32554  iszeroo  32608  iszeroi  32615  rnghmval2  32701  rnghmsubcsetclem1  32783  rngccatidOLD  32797  funcrngcsetcALT  32807  zrinitorngc  32808  zrtermorngc  32809  rhmsubcsetclem1  32829  rhmsubcrngclem1  32835  ringcbasbas  32842  funcringcsetcOLD2lem7  32850  ringccatidOLD  32860  ringcbasbasOLD  32866  funcringcsetclem7OLD  32873  irinitoringc  32877  zrtermoringc  32878  srhmsubclem1  32881  fldhmsubc  32892  srhmsubcOLDlem1  32900  fldhmsubcOLD  32911  rhmsubcOLDlem3  32915  ssnn0ssfz  32938  onfrALTlem2  33318  onfrALTlem2VD  33689  bnj521  33792  bnj1172  34057  bnj1173  34058  bnj1174  34059  bnj1279  34074  bj-inrab  34495  bj-eldiag  34606  bj-eldiag2  34607  bj-ccinftydisj  34616  lshpdisj  34712  lkrin  34889  ishlat1  35077  pmodlem2  35571  pclfinN  35624  pclcmpatN  35625  osumcllem4N  35683  pexmidlem1N  35694  dihmeetlem1N  37017  dihglblem5apreN  37018  dihmeetlem4preN  37033  dihmeetlem13N  37046  dochnel2  37119  lcdlss  37346  mapd1o  37375  baerlem3lem2  37437  baerlem5alem2  37438  baerlem5blem2  37439  taupilem3  37694  rp-fakeinunass  37740  fiinfi  37758  xpcogend  37773  cotr2g  37786  ndisj  37793
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1618  ax-4 1631  ax-5 1704  ax-6 1747  ax-7 1790  ax-10 1837  ax-11 1842  ax-12 1854  ax-13 1999  ax-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-sb 1740  df-clab 2443  df-cleq 2449  df-clel 2452  df-nfc 2607  df-v 3111  df-in 3482
  Copyright terms: Public domain W3C validator