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

Theorem nfel1 2604
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 2589 . 2  |-  F/_ x B
31, 2nfel 2601 1  |-  F/ x  A  e.  B
Colors of variables: wff setvar class
Syntax hints:   F/wnf 1589    e. wcel 1756   F/_wnfc 2575
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-10 1775  ax-11 1780  ax-12 1792  ax-ext 2423
This theorem depends on definitions:  df-bi 185  df-an 371  df-tru 1372  df-ex 1587  df-nf 1590  df-cleq 2436  df-clel 2439  df-nfc 2577
This theorem is referenced by:  vtocl2gf  3047  vtocl3gf  3048  vtoclgaf  3050  vtocl2gaf  3052  vtocl3gaf  3054  nfop  4090  reusv2lem4  4511  reusv2  4513  rabxfrd  4528  pofun  4672  nfse  4710  fvmptf  5805  fmptcof  5892  fliftfuns  6022  riota2f  6089  ovmpt2s  6229  ov2gf  6230  ofmpteq  6353  fmpt2x  6655  offval22  6667  fvmpt2curryd  6805  qliftfuns  7202  xpf1o  7488  iunfi  7614  wdom2d  7810  scottex  8107  dfac8clem  8217  ac6num  8663  pwfseqlem4a  8843  pwfseqlem4  8844  gruiin  8992  rlimcld2  13071  summolem3  13206  summolem2a  13207  zsum  13210  fsum  13212  sumss2  13218  fsumcvg2  13219  fsum2dlem  13252  fsumcom2  13256  fsumshftm  13263  fsum0diag2  13265  fsum00  13276  fsumabs  13279  fsumrlim  13289  fsumo1  13290  o1fsum  13291  fsumiun  13299  pcmpt  13969  pcmptdvds  13971  dprdwd  16510  dprdwdOLD  16516  mdetralt2  18430  mdetunilem2  18434  fiuncmp  19022  elptr2  19162  ptcld  19201  ptcnplem  19209  ptcnp  19210  elmptrab  19415  utopsnneiplem  19837  prdsdsf  19957  prdsxmet  19959  fsumcn  20461  ovolfiniun  20999  ovoliunlem3  21002  ovoliun  21003  ovoliun2  21004  finiunmbl  21040  volfiniun  21043  iunmbl  21049  voliun  21050  itgfsum  21319  itgabs  21327  dvmptfsum  21462  dvfsumle  21508  dvfsumabs  21510  dvfsumlem1  21513  dvfsumlem3  21515  dvfsumlem4  21516  dvfsumrlim  21518  dvfsumrlim2  21519  dvfsum2  21521  itgsubst  21536  fsumdvdscom  22540  fsumvma  22567  dchrisumlema  22752  dchrisumlem2  22754  dchrisumlem3  22755  suppss2f  25969  esumcl  26501  esum0  26518  esumcst  26529  esumfsup  26534  measiun  26647  voliune  26660  volfiniune  26661  iota5f  27396  prodmolem3  27461  prodmolem2a  27462  zprod  27465  fprod  27469  prodss  27475  fprodser  27477  fprodm1s  27495  fprodp1s  27496  fprodabs  27499  fprodefsum  27500  fprodn0  27505  fprod2dlem  27506  fprodcom2  27510  itgabsnc  28480  mzpsubmpt  29098  mzpsubst  29104  eq0rabdioph  29134  eqrabdioph  29135  rabdiophlem2  29159  fphpd  29174  monotuz  29301  monotoddzz  29303  oddcomabszz  29304  flcidc  29550  rfcnnnub  29777  fmul01  29780  fmuldfeqlem1  29782  fmuldfeq  29783  fmul01lt1lem1  29784  fmul01lt1lem2  29785  climmulf  29796  climsuse  29800  climrecf  29801  stoweidlem3  29817  stoweidlem19  29833  stoweidlem22  29836  stoweidlem42  29856  eu2ndop1stv  30045  elovmpt2rab  30177  elovmpt2rab1  30178  fsumshftd  32621  fsumshftdOLD  32622  riotasv2s  32628  cdlemefs32sn1aw  34077
  Copyright terms: Public domain W3C validator