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

Theorem nfel1 2601
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1  |-  F/_ x A
Assertion
Ref Expression
nfel1  |-  F/ x  A  e.  B
Distinct variable group:    x, B
Allowed substitution hint:    A( x)

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2  |-  F/_ x A
2 nfcv 2585 . 2  |-  F/_ x B
31, 2nfel 2598 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1664    e. wcel 1869   F/_wnfc 2571
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1666  ax-4 1679  ax-5 1749  ax-6 1795  ax-7 1840  ax-10 1888  ax-11 1893  ax-12 1906  ax-ext 2401
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1441  df-ex 1661  df-nf 1665  df-cleq 2415  df-clel 2418  df-nfc 2573
This theorem is referenced by:  vtocl2gf  3142  vtocl3gf  3143  vtoclgaf  3145  vtocl2gaf  3147  vtocl3gaf  3149  nfop  4201  reusv2lem4  4626  reusv2  4628  rabxfrd  4640  pofun  4788  nfse  4826  fvmptf  5980  fmptcof  6070  fliftfuns  6220  riota2f  6286  ovmpt2s  6432  ov2gf  6433  elovmpt2rab  6527  elovmpt2rab1  6528  ofmpteq  6562  fmpt2x  6871  offval22  6884  fvmpt2curryd  7024  qliftfuns  7456  xpf1o  7738  iunfi  7866  wdom2d  8099  scottex  8359  dfac8clem  8465  ac6num  8911  pwfseqlem4a  9088  pwfseqlem4  9089  gruiin  9237  rlimcld2  13635  summolem3  13773  summolem2a  13774  zsum  13777  fsum  13779  sumss2  13785  fsumcvg2  13786  fsum2dlem  13824  fsumcom2  13828  fsumshftm  13835  fsum0diag2  13837  fsum00  13851  fsumabs  13854  fsumrlim  13864  fsumo1  13865  o1fsum  13866  fsumiun  13874  prodmolem3  13980  prodmolem2a  13981  zprod  13984  fprod  13988  prodss  13994  fprodser  13996  fprodm1s  14017  fprodp1s  14018  fprodabs  14021  fprodn0  14026  fprod2dlem  14027  fprodcom2  14031  fprodsplitf  14035  fprodefsum  14142  pcmpt  14830  pcmptdvds  14832  gsumsnf  17579  dprdwdOLD  17637  gsumply1eq  18892  mdetralt2  19626  mdetunilem2  19630  fiuncmp  20411  elptr2  20581  ptcld  20620  ptcnplem  20628  ptcnp  20629  elmptrab  20834  utopsnneiplem  21254  prdsdsf  21374  prdsxmet  21376  fsumcn  21894  ovolfiniun  22446  ovoliunlem3  22449  ovoliun  22450  ovoliun2  22451  finiunmbl  22489  volfiniun  22492  iunmbl  22498  voliun  22499  itgfsum  22776  itgabs  22784  dvmptfsum  22919  dvfsumle  22965  dvfsumabs  22967  dvfsumlem1  22970  dvfsumlem3  22972  dvfsumlem4  22973  dvfsumrlim  22975  dvfsumrlim2  22976  dvfsum2  22978  itgsubst  22993  fsumdvdscom  24106  fsumvma  24133  dchrisumlema  24318  dchrisumlem2  24320  dchrisumlem3  24321  suppss2fOLD  28233  locfinreflem  28669  esumcl  28853  esum0  28872  esumcst  28886  esumfsup  28893  esum2d  28916  measiun  29042  voliune  29054  volfiniune  29055  iota5f  30359  phpreu  31849  poimirlem25  31885  poimirlem26  31886  poimirlem28  31888  itgabsnc  31931  fsumshftd  32448  fsumshftdOLD  32449  riotasv2s  32455  cdlemefs32sn1aw  33906  mzpsubmpt  35510  mzpsubst  35515  eq0rabdioph  35544  eqrabdioph  35545  rabdiophlem2  35570  fphpd  35584  monotuz  35715  monotoddzz  35717  oddcomabszz  35718  flcidc  35966  binomcxplemdvbinom  36566  binomcxplemdvsum  36568  binomcxplemnotnn0  36569  rfcnnnub  37224  fsumclf  37474  fsumsplitf  37475  fsummulc1f  37476  fsumnncl  37479  fsumf1of  37482  fmul01  37484  fmuldfeqlem1  37486  fmuldfeq  37487  fmul01lt1lem1  37488  fmul01lt1lem2  37489  fprodexp  37500  fprodabs2  37501  climmulf  37508  climsuse  37513  climrecf  37514  climaddf  37521  0ellimcdiv  37556  fprodcncf  37605  dvmptmulf  37638  iblspltprt  37676  stoweidlem3  37689  stoweidlem19  37705  stoweidlem22  37708  stoweidlem42  37729  fourierdlem31  37826  fourierdlem31OLD  37827  fourierdlem86  37882  fourierdlem89  37885  fourierdlem91  37887  fourierdlem112  37908  sge0f1o  38018  sge0lempt  38046  sge0iunmpt  38054  sge0ltfirpmpt2  38062  sge0isummpt2  38068  sge0xaddlem2  38070  sge0xadd  38071  eu2ndop1stv  38342
  Copyright terms: Public domain W3C validator