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

Theorem nfel1 2550
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 2540 . 2  |-  F/_ x B
31, 2nfel 2548 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1550    e. wcel 1721   F/_wnfc 2527
This theorem is referenced by:  vtocl2gf  2973  vtocl3gf  2974  vtoclgaf  2976  vtocl2gaf  2978  vtocl3gaf  2980  nfop  3960  pofun  4479  nfse  4517  reusv2lem4  4686  reusv2  4688  rabxfrd  4703  fvmptf  5780  fmptcof  5861  fliftfuns  5995  ovmpt2s  6156  ov2gf  6157  fmpt2x  6376  riota2f  6530  riotasv2s  6555  qliftfuns  6950  xpf1o  7228  iunfi  7353  wdom2d  7504  scottex  7765  dfac8clem  7869  ac6num  8315  pwfseqlem4a  8492  pwfseqlem4  8493  gruiin  8641  rlimcld2  12327  summolem3  12463  summolem2a  12464  zsum  12467  fsum  12469  sumss2  12475  fsumcvg2  12476  fsum2dlem  12509  fsumcom2  12513  fsumshftm  12519  fsum0diag2  12521  fsum00  12532  fsumabs  12535  fsumrlim  12545  fsumo1  12546  o1fsum  12547  fsumiun  12555  pcmpt  13216  pcmptdvds  13218  dprdwd  15524  fiuncmp  17421  elptr2  17559  ptcld  17598  ptcnplem  17606  ptcnp  17607  elmptrab  17812  utopsnneiplem  18230  prdsdsf  18350  prdsxmet  18352  fsumcn  18853  ovolfiniun  19350  ovoliunlem3  19353  ovoliun  19354  ovoliun2  19355  finiunmbl  19391  volfiniun  19394  iunmbl  19400  voliun  19401  itgfsum  19671  itgabs  19679  dvmptfsum  19812  dvfsumle  19858  dvfsumabs  19860  dvfsumlem1  19863  dvfsumlem3  19865  dvfsumlem4  19866  dvfsumrlim  19868  dvfsumrlim2  19869  dvfsum2  19871  itgsubst  19886  fsumdvdscom  20923  fsumvma  20950  dchrisumlema  21135  dchrisumlem2  21137  dchrisumlem3  21138  suppss2f  24002  esumcl  24380  esum0  24397  esumcst  24408  esumfsup  24413  measiun  24525  voliune  24538  volfiniune  24539  iota5f  25135  prodmolem3  25212  prodmolem2a  25213  zprod  25216  fprod  25220  prodss  25226  fprodser  25228  fprodm1s  25246  fprodp1s  25247  fprodabs  25250  fprodefsum  25251  fprodn0  25256  fprod2dlem  25257  fprodcom2  25261  itgabsnc  26173  ofmpteq  26666  mzpsubmpt  26690  mzpsubst  26695  eq0rabdioph  26725  eqrabdioph  26726  rabdiophlem2  26752  fphpd  26767  monotuz  26894  monotoddzz  26896  oddcomabszz  26897  flcidc  27247  rfcnnnub  27574  fmul01  27577  fmuldfeqlem1  27579  fmuldfeq  27580  fmul01lt1lem1  27581  fmul01lt1lem2  27582  climmulf  27597  climsuse  27601  climrecf  27602  stoweidlem3  27619  stoweidlem19  27635  stoweidlem22  27638  stoweidlem42  27658  eu2ndop1stv  27847  cdlemefs32sn1aw  30896
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2385
This theorem depends on definitions:  df-bi 178  df-an 361  df-tru 1325  df-ex 1548  df-nf 1551  df-sb 1656  df-cleq 2397  df-clel 2400  df-nfc 2529
  Copyright terms: Public domain W3C validator