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

Theorem nfel1 2621
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 2605 . 2  |-  F/_ x B
31, 2nfel 2618 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1603    e. wcel 1804   F/_wnfc 2591
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1605  ax-4 1618  ax-5 1691  ax-6 1734  ax-7 1776  ax-10 1823  ax-11 1828  ax-12 1840  ax-ext 2421
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1386  df-ex 1600  df-nf 1604  df-cleq 2435  df-clel 2438  df-nfc 2593
This theorem is referenced by:  vtocl2gf  3155  vtocl3gf  3156  vtoclgaf  3158  vtocl2gaf  3160  vtocl3gaf  3162  nfop  4218  reusv2lem4  4641  reusv2  4643  rabxfrd  4658  pofun  4806  nfse  4844  fvmptf  5957  fmptcof  6050  fliftfuns  6197  riota2f  6264  ovmpt2s  6411  ov2gf  6412  elovmpt2rab  6506  elovmpt2rab1  6507  ofmpteq  6543  fmpt2x  6851  offval22  6864  fvmpt2curryd  7002  qliftfuns  7400  xpf1o  7681  iunfi  7810  wdom2d  8009  scottex  8306  dfac8clem  8416  ac6num  8862  pwfseqlem4a  9042  pwfseqlem4  9043  gruiin  9191  rlimcld2  13383  summolem3  13518  summolem2a  13519  zsum  13522  fsum  13524  sumss2  13530  fsumcvg2  13531  fsum2dlem  13567  fsumcom2  13571  fsumshftm  13578  fsum0diag2  13580  fsum00  13594  fsumabs  13597  fsumrlim  13607  fsumo1  13608  o1fsum  13609  fsumiun  13617  prodmolem3  13722  prodmolem2a  13723  zprod  13726  fprod  13730  prodss  13736  fprodser  13738  fprodm1s  13756  fprodp1s  13757  fprodabs  13760  fprodn0  13765  fprod2dlem  13766  fprodcom2  13770  fprodefsum  13812  pcmpt  14393  pcmptdvds  14395  gsumsnf  16959  dprdwdOLD2  17024  dprdwdOLD  17030  gsumply1eq  18326  mdetralt2  19089  mdetunilem2  19093  fiuncmp  19882  elptr2  20053  ptcld  20092  ptcnplem  20100  ptcnp  20101  elmptrab  20306  utopsnneiplem  20728  prdsdsf  20848  prdsxmet  20850  fsumcn  21352  ovolfiniun  21890  ovoliunlem3  21893  ovoliun  21894  ovoliun2  21895  finiunmbl  21932  volfiniun  21935  iunmbl  21941  voliun  21942  itgfsum  22211  itgabs  22219  dvmptfsum  22354  dvfsumle  22400  dvfsumabs  22402  dvfsumlem1  22405  dvfsumlem3  22407  dvfsumlem4  22408  dvfsumrlim  22410  dvfsumrlim2  22411  dvfsum2  22413  itgsubst  22428  fsumdvdscom  23439  fsumvma  23466  dchrisumlema  23651  dchrisumlem2  23653  dchrisumlem3  23654  suppss2f  27455  locfinreflem  27821  esumcl  28021  esum0  28038  esumcst  28049  esumfsup  28054  measiun  28167  voliune  28179  volfiniune  28180  iota5f  29080  itgabsnc  30060  mzpsubmpt  30651  mzpsubst  30657  eq0rabdioph  30686  eqrabdioph  30687  rabdiophlem2  30711  fphpd  30726  monotuz  30853  monotoddzz  30855  oddcomabszz  30856  flcidc  31099  rfcnnnub  31365  fsumclf  31521  fsumsplitf  31522  fsummulc1f  31523  fsumnncl  31526  fmul01  31528  fmuldfeqlem1  31530  fmuldfeq  31531  fmul01lt1lem1  31532  fmul01lt1lem2  31533  fprodsplitf  31543  fprodexp  31554  fprodabs2  31556  climmulf  31564  climsuse  31568  climrecf  31569  climaddf  31575  0ellimcdiv  31609  fprodcncf  31658  dvmptmulf  31688  iblspltprt  31726  stoweidlem3  31739  stoweidlem19  31755  stoweidlem22  31758  stoweidlem42  31778  fourierdlem31  31874  fourierdlem86  31929  fourierdlem89  31932  fourierdlem91  31934  fourierdlem112  31955  eu2ndop1stv  32161  fsumshftd  34557  fsumshftdOLD  34558  riotasv2s  34564  cdlemefs32sn1aw  36015
  Copyright terms: Public domain W3C validator