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

Theorem nfel1 2582
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 2566 . 2  |-  F/_ x B
31, 2nfel 2579 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1639    e. wcel 1844   F/_wnfc 2552
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1641  ax-4 1654  ax-5 1727  ax-6 1773  ax-7 1816  ax-10 1863  ax-11 1868  ax-12 1880  ax-ext 2382
This theorem depends on definitions:  df-bi 187  df-an 371  df-tru 1410  df-ex 1636  df-nf 1640  df-cleq 2396  df-clel 2399  df-nfc 2554
This theorem is referenced by:  vtocl2gf  3121  vtocl3gf  3122  vtoclgaf  3124  vtocl2gaf  3126  vtocl3gaf  3128  nfop  4177  reusv2lem4  4600  reusv2  4602  rabxfrd  4614  pofun  4762  nfse  4800  fvmptf  5952  fmptcof  6046  fliftfuns  6197  riota2f  6263  ovmpt2s  6409  ov2gf  6410  elovmpt2rab  6504  elovmpt2rab1  6505  ofmpteq  6542  fmpt2x  6852  offval22  6865  fvmpt2curryd  7005  qliftfuns  7437  xpf1o  7719  iunfi  7844  wdom2d  8042  scottex  8337  dfac8clem  8447  ac6num  8893  pwfseqlem4a  9071  pwfseqlem4  9072  gruiin  9220  rlimcld2  13552  summolem3  13687  summolem2a  13688  zsum  13691  fsum  13693  sumss2  13699  fsumcvg2  13700  fsum2dlem  13738  fsumcom2  13742  fsumshftm  13749  fsum0diag2  13751  fsum00  13765  fsumabs  13768  fsumrlim  13778  fsumo1  13779  o1fsum  13780  fsumiun  13788  prodmolem3  13894  prodmolem2a  13895  zprod  13898  fprod  13902  prodss  13908  fprodser  13910  fprodm1s  13928  fprodp1s  13929  fprodabs  13932  fprodn0  13937  fprod2dlem  13938  fprodcom2  13942  fprodefsum  14041  pcmpt  14622  pcmptdvds  14624  gsumsnf  17303  dprdwdOLD2  17367  dprdwdOLD  17373  gsumply1eq  18669  mdetralt2  19405  mdetunilem2  19409  fiuncmp  20199  elptr2  20369  ptcld  20408  ptcnplem  20416  ptcnp  20417  elmptrab  20622  utopsnneiplem  21044  prdsdsf  21164  prdsxmet  21166  fsumcn  21668  ovolfiniun  22206  ovoliunlem3  22209  ovoliun  22210  ovoliun2  22211  finiunmbl  22248  volfiniun  22251  iunmbl  22257  voliun  22258  itgfsum  22527  itgabs  22535  dvmptfsum  22670  dvfsumle  22716  dvfsumabs  22718  dvfsumlem1  22721  dvfsumlem3  22723  dvfsumlem4  22724  dvfsumrlim  22726  dvfsumrlim2  22727  dvfsum2  22729  itgsubst  22744  fsumdvdscom  23844  fsumvma  23871  dchrisumlema  24056  dchrisumlem2  24058  dchrisumlem3  24059  suppss2f  27933  locfinreflem  28309  esumcl  28490  esum0  28509  esumcst  28523  esumfsup  28530  esum2d  28553  measiun  28679  voliune  28691  volfiniune  28692  iota5f  29944  itgabsnc  31470  fsumshftd  31988  fsumshftdOLD  31989  riotasv2s  31995  cdlemefs32sn1aw  33446  mzpsubmpt  35050  mzpsubst  35055  eq0rabdioph  35084  eqrabdioph  35085  rabdiophlem2  35110  fphpd  35124  monotuz  35251  monotoddzz  35253  oddcomabszz  35254  flcidc  35500  binomcxplemdvbinom  36119  binomcxplemdvsum  36121  binomcxplemnotnn0  36122  rfcnnnub  36804  fsumclf  36948  fsumsplitf  36949  fsummulc1f  36950  fsumnncl  36953  fmul01  36955  fmuldfeqlem1  36957  fmuldfeq  36958  fmul01lt1lem1  36959  fmul01lt1lem2  36960  fprodsplitf  36970  fprodexp  36981  fprodabs2  36983  climmulf  36991  climsuse  36995  climrecf  36996  climaddf  37002  0ellimcdiv  37036  fprodcncf  37085  dvmptmulf  37115  iblspltprt  37153  stoweidlem3  37166  stoweidlem19  37182  stoweidlem22  37185  stoweidlem42  37205  fourierdlem31  37301  fourierdlem86  37356  fourierdlem89  37359  fourierdlem91  37361  fourierdlem112  37382  eu2ndop1stv  37588
  Copyright terms: Public domain W3C validator