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

Theorem nfel1 2606
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 2592 . 2  |-  F/_ x B
31, 2nfel 2604 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1667    e. wcel 1887   F/_wnfc 2579
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1669  ax-4 1682  ax-5 1758  ax-6 1805  ax-7 1851  ax-10 1915  ax-11 1920  ax-12 1933  ax-ext 2431
This theorem depends on definitions:  df-bi 189  df-an 373  df-tru 1447  df-ex 1664  df-nf 1668  df-cleq 2444  df-clel 2447  df-nfc 2581
This theorem is referenced by:  vtocl2gf  3109  vtocl3gf  3110  vtoclgaf  3112  vtocl2gaf  3114  vtocl3gaf  3116  nfop  4182  reusv2lem4  4607  reusv2  4609  rabxfrd  4621  pofun  4771  nfse  4809  fvmptf  5966  fmptcof  6057  fliftfuns  6207  riota2f  6273  ovmpt2s  6420  ov2gf  6421  elovmpt2rab  6515  elovmpt2rab1  6516  ofmpteq  6550  fmpt2x  6859  offval22  6872  fvmpt2curryd  7018  qliftfuns  7450  xpf1o  7734  iunfi  7862  wdom2d  8095  scottex  8356  dfac8clem  8463  ac6num  8909  pwfseqlem4a  9086  pwfseqlem4  9087  gruiin  9235  rlimcld2  13642  summolem3  13780  summolem2a  13781  zsum  13784  fsum  13786  sumss2  13792  fsumcvg2  13793  fsum2dlem  13831  fsumcom2  13835  fsumshftm  13842  fsum0diag2  13844  fsum00  13858  fsumabs  13861  fsumrlim  13871  fsumo1  13872  o1fsum  13873  fsumiun  13881  prodmolem3  13987  prodmolem2a  13988  zprod  13991  fprod  13995  prodss  14001  fprodser  14003  fprodm1s  14024  fprodp1s  14025  fprodabs  14028  fprodn0  14033  fprod2dlem  14034  fprodcom2  14038  fprodsplitf  14042  fprodefsum  14149  pcmpt  14837  pcmptdvds  14839  gsumsnf  17586  dprdwdOLD  17644  gsumply1eq  18899  mdetralt2  19634  mdetunilem2  19638  fiuncmp  20419  elptr2  20589  ptcld  20628  ptcnplem  20636  ptcnp  20637  elmptrab  20842  utopsnneiplem  21262  prdsdsf  21382  prdsxmet  21384  fsumcn  21902  ovolfiniun  22454  ovoliunlem3  22457  ovoliun  22458  ovoliun2  22459  finiunmbl  22497  volfiniun  22500  iunmbl  22506  voliun  22507  itgfsum  22784  itgabs  22792  dvmptfsum  22927  dvfsumle  22973  dvfsumabs  22975  dvfsumlem1  22978  dvfsumlem3  22980  dvfsumlem4  22981  dvfsumrlim  22983  dvfsumrlim2  22984  dvfsum2  22986  itgsubst  23001  fsumdvdscom  24114  fsumvma  24141  dchrisumlema  24326  dchrisumlem2  24328  dchrisumlem3  24329  suppss2fOLD  28237  locfinreflem  28667  esumcl  28851  esum0  28870  esumcst  28884  esumfsup  28891  esum2d  28914  measiun  29040  voliune  29052  volfiniune  29053  iota5f  30357  phpreu  31929  poimirlem25  31965  poimirlem26  31966  poimirlem28  31968  itgabsnc  32011  fsumshftd  32523  fsumshftdOLD  32524  riotasv2s  32530  cdlemefs32sn1aw  33981  mzpsubmpt  35585  mzpsubst  35590  eq0rabdioph  35619  eqrabdioph  35620  rabdiophlem2  35645  fphpd  35659  monotuz  35789  monotoddzz  35791  oddcomabszz  35792  flcidc  36040  binomcxplemdvbinom  36702  binomcxplemdvsum  36704  binomcxplemnotnn0  36705  rfcnnnub  37357  fsumclf  37645  fsumsplitf  37646  fsummulc1f  37647  fsumnncl  37650  fsumf1of  37653  fsumreclf  37655  fsumlessf  37656  fmul01  37658  fmuldfeqlem1  37660  fmuldfeq  37661  fmul01lt1lem1  37662  fmul01lt1lem2  37663  fprodexp  37674  fprodabs2  37675  climmulf  37682  climsuse  37687  climrecf  37688  climaddf  37695  0ellimcdiv  37730  fprodcncf  37779  dvmptmulf  37812  iblspltprt  37850  stoweidlem3  37863  stoweidlem19  37879  stoweidlem22  37882  stoweidlem42  37903  fourierdlem31  38000  fourierdlem31OLD  38001  fourierdlem86  38056  fourierdlem89  38059  fourierdlem91  38061  fourierdlem112  38082  sge0f1o  38224  sge0lempt  38252  sge0iunmpt  38260  sge0ltfirpmpt2  38268  sge0isummpt2  38274  sge0xaddlem2  38276  sge0xadd  38277  eu2ndop1stv  38623
  Copyright terms: Public domain W3C validator