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

Theorem nfel1 2442
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 2432 . 2  |-  F/_ x B
31, 2nfel 2440 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1534    e. wcel 1696   F/_wnfc 2419
This theorem is referenced by:  vtocl2gf  2858  vtocl3gf  2859  vtoclgaf  2861  vtocl2gaf  2863  vtocl3gaf  2865  nfop  3828  pofun  4346  nfse  4384  reusv2lem4  4554  reusv2  4556  rabxfrd  4571  fvmptf  5632  fmptcof  5708  fliftfuns  5829  ovmpt2s  5987  ov2gf  5988  fmpt2x  6206  riota2f  6342  riotasv2s  6367  qliftfuns  6761  xpf1o  7039  iunfi  7160  wdom2d  7310  scottex  7571  dfac8clem  7675  ac6num  8122  pwfseqlem4a  8299  pwfseqlem4  8300  gruiin  8448  rlimcld2  12068  summolem3  12203  summolem2a  12204  zsum  12207  fsum  12209  sumss2  12215  fsumcvg2  12216  fsum2dlem  12249  fsumcom2  12253  fsumshftm  12259  fsum0diag2  12261  fsum00  12272  fsumabs  12275  fsumrlim  12285  fsumo1  12286  o1fsum  12287  fsumiun  12295  pcmpt  12956  pcmptdvds  12958  dprdwd  15262  fiuncmp  17147  elptr2  17285  ptcld  17323  ptcnplem  17331  ptcnp  17332  elmptrab  17538  prdsdsf  17947  prdsxmet  17949  fsumcn  18390  ovolfiniun  18876  ovoliunlem3  18879  ovoliun  18880  ovoliun2  18881  finiunmbl  18917  volfiniun  18920  iunmbl  18926  voliun  18927  itgfsum  19197  itgabs  19205  dvmptfsum  19338  dvfsumle  19384  dvfsumabs  19386  dvfsumlem1  19389  dvfsumlem3  19391  dvfsumlem4  19392  dvfsumrlim  19394  dvfsumrlim2  19395  dvfsum2  19397  itgsubst  19412  fsumdvdscom  20441  fsumvma  20468  dchrisumlema  20653  dchrisumlem2  20655  dchrisumlem3  20656  measiun  23560  prodmolem3  24156  prodmolem2a  24157  zprod  24160  fprod  24164  itgabsnc  25020  ofmpteq  26900  mzpsubmpt  26924  mzpsubst  26929  eq0rabdioph  26959  eqrabdioph  26960  rabdiophlem2  26986  fphpd  27002  monotuz  27129  monotoddzz  27131  oddcomabszz  27132  climsuse  27837  cdlemefs32sn1aw  31225  cdlemk36  31724
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1536  ax-5 1547  ax-17 1606  ax-9 1644  ax-8 1661  ax-6 1715  ax-7 1720  ax-11 1727  ax-12 1878  ax-ext 2277
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1532  df-nf 1535  df-sb 1639  df-cleq 2289  df-clel 2292  df-nfc 2421
  Copyright terms: Public domain W3C validator