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

Theorem nfel1 2635
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq1.1
Assertion
Ref Expression
nfel1
Distinct variable group:   ,

Proof of Theorem nfel1
StepHypRef Expression
1 nfeq1.1 . 2
2 nfcv 2619 . 2
31, 2nfel 2632 1
Colors of variables: wff setvar class
Syntax hints:  F/wnf 1616  e.wcel 1818  F/_wnfc 2605
This theorem is referenced by:  vtocl2gf  3169  vtocl3gf  3170  vtoclgaf  3172  vtocl2gaf  3174  vtocl3gaf  3176  nfop  4233  reusv2lem4  4656  reusv2  4658  rabxfrd  4673  pofun  4821  nfse  4859  fvmptf  5972  fmptcof  6065  fliftfuns  6212  riota2f  6279  ovmpt2s  6426  ov2gf  6427  elovmpt2rab  6521  elovmpt2rab1  6522  ofmpteq  6558  fmpt2x  6866  offval22  6879  fvmpt2curryd  7019  qliftfuns  7417  xpf1o  7699  iunfi  7828  wdom2d  8027  scottex  8324  dfac8clem  8434  ac6num  8880  pwfseqlem4a  9060  pwfseqlem4  9061  gruiin  9209  rlimcld2  13401  summolem3  13536  summolem2a  13537  zsum  13540  fsum  13542  sumss2  13548  fsumcvg2  13549  fsum2dlem  13585  fsumcom2  13589  fsumshftm  13596  fsum0diag2  13598  fsum00  13612  fsumabs  13615  fsumrlim  13625  fsumo1  13626  o1fsum  13627  fsumiun  13635  prodmolem3  13740  prodmolem2a  13741  zprod  13744  fprod  13748  prodss  13754  fprodser  13756  fprodm1s  13774  fprodp1s  13775  fprodabs  13778  fprodn0  13783  fprod2dlem  13784  fprodcom2  13788  fprodefsum  13830  pcmpt  14411  pcmptdvds  14413  gsumsnf  16980  dprdwdOLD2  17045  dprdwdOLD  17051  gsumply1eq  18347  mdetralt2  19111  mdetunilem2  19115  fiuncmp  19904  elptr2  20075  ptcld  20114  ptcnplem  20122  ptcnp  20123  elmptrab  20328  utopsnneiplem  20750  prdsdsf  20870  prdsxmet  20872  fsumcn  21374  ovolfiniun  21912  ovoliunlem3  21915  ovoliun  21916  ovoliun2  21917  finiunmbl  21954  volfiniun  21957  iunmbl  21963  voliun  21964  itgfsum  22233  itgabs  22241  dvmptfsum  22376  dvfsumle  22422  dvfsumabs  22424  dvfsumlem1  22427  dvfsumlem3  22429  dvfsumlem4  22430  dvfsumrlim  22432  dvfsumrlim2  22433  dvfsum2  22435  itgsubst  22450  fsumdvdscom  23461  fsumvma  23488  dchrisumlema  23673  dchrisumlem2  23675  dchrisumlem3  23676  suppss2f  27477  locfinreflem  27843  esumcl  28043  esum0  28060  esumcst  28071  esumfsup  28076  measiun  28189  voliune  28201  volfiniune  28202  iota5f  29102  itgabsnc  30084  mzpsubmpt  30675  mzpsubst  30681  eq0rabdioph  30710  eqrabdioph  30711  rabdiophlem2  30735  fphpd  30750  monotuz  30877  monotoddzz  30879  oddcomabszz  30880  flcidc  31123  binomcxplemdvbinom  31258  binomcxplemdvsum  31260  binomcxplemnotnn0  31261  rfcnnnub  31411  fsumclf  31567  fsumsplitf  31568  fsummulc1f  31569  fsumnncl  31572  fmul01  31574  fmuldfeqlem1  31576  fmuldfeq  31577  fmul01lt1lem1  31578  fmul01lt1lem2  31579  fprodsplitf  31589  fprodexp  31600  fprodabs2  31602  climmulf  31610  climsuse  31614  climrecf  31615  climaddf  31621  0ellimcdiv  31655  fprodcncf  31704  dvmptmulf  31734  iblspltprt  31772  stoweidlem3  31785  stoweidlem19  31801  stoweidlem22  31804  stoweidlem42  31824  fourierdlem31  31920  fourierdlem86  31975  fourierdlem89  31978  fourierdlem91  31980  fourierdlem112  32001  eu2ndop1stv  32207  fsumshftd  34682  fsumshftdOLD  34683  riotasv2s  34689  cdlemefs32sn1aw  36140
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-ext 2435
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1398  df-ex 1613  df-nf 1617  df-cleq 2449  df-clel 2452  df-nfc 2607
  Copyright terms: Public domain W3C validator