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

Theorem nfel1 2429
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 2419 . 2  |-  F/_ x B
31, 2nfel 2427 1  |-  F/ x  A  e.  B
Colors of variables: wff set class
Syntax hints:   F/wnf 1531    e. wcel 1684   F/_wnfc 2406
This theorem is referenced by:  vtocl2gf  2845  vtocl3gf  2846  vtoclgaf  2848  vtocl2gaf  2850  vtocl3gaf  2852  nfop  3812  pofun  4330  nfse  4368  reusv2lem4  4538  reusv2  4540  rabxfrd  4555  fvmptf  5616  fmptcof  5692  fliftfuns  5813  ovmpt2s  5971  ov2gf  5972  fmpt2x  6190  riota2f  6326  riotasv2s  6351  qliftfuns  6745  xpf1o  7023  iunfi  7144  wdom2d  7294  scottex  7555  dfac8clem  7659  ac6num  8106  pwfseqlem4a  8283  pwfseqlem4  8284  gruiin  8432  rlimcld2  12052  summolem3  12187  summolem2a  12188  zsum  12191  fsum  12193  sumss2  12199  fsumcvg2  12200  fsum2dlem  12233  fsumcom2  12237  fsumshftm  12243  fsum0diag2  12245  fsum00  12256  fsumabs  12259  fsumrlim  12269  fsumo1  12270  o1fsum  12271  fsumiun  12279  pcmpt  12940  pcmptdvds  12942  dprdwd  15246  fiuncmp  17131  elptr2  17269  ptcld  17307  ptcnplem  17315  ptcnp  17316  elmptrab  17522  prdsdsf  17931  prdsxmet  17933  fsumcn  18374  ovolfiniun  18860  ovoliunlem3  18863  ovoliun  18864  ovoliun2  18865  finiunmbl  18901  volfiniun  18904  iunmbl  18910  voliun  18911  itgfsum  19181  itgabs  19189  dvmptfsum  19322  dvfsumle  19368  dvfsumabs  19370  dvfsumlem1  19373  dvfsumlem3  19375  dvfsumlem4  19376  dvfsumrlim  19378  dvfsumrlim2  19379  dvfsum2  19381  itgsubst  19396  fsumdvdscom  20425  fsumvma  20452  dchrisumlema  20637  dchrisumlem2  20639  dchrisumlem3  20640  ofmpteq  26209  mzpsubmpt  26233  mzpsubst  26238  eq0rabdioph  26268  eqrabdioph  26269  rabdiophlem2  26295  fphpd  26311  monotuz  26438  monotoddzz  26440  oddcomabszz  26441  climsuse  27146  cdlemefs32sn1aw  29976  cdlemk36  30475
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264
This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-cleq 2276  df-clel 2279  df-nfc 2408
  Copyright terms: Public domain W3C validator