MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  nfel2 Structured version   Visualization version   GIF version

Theorem nfel2 2921
Description: Hypothesis builder for elementhood, special case. (Contributed by Mario Carneiro, 10-Oct-2016.)
Hypothesis
Ref Expression
nfeq2.1 𝑥𝐵
Assertion
Ref Expression
nfel2 𝑥 𝐴𝐵
Distinct variable group:   𝑥,𝐴
Allowed substitution hint:   𝐵(𝑥)

Proof of Theorem nfel2
StepHypRef Expression
1 nfcv 2903 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2917 1 𝑥 𝐴𝐵
Colors of variables: wff setvar class
Syntax hints:  wnf 1785  wcel 2106  wnfc 2883
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1797  ax-4 1811  ax-5 1913  ax-6 1971  ax-7 2011  ax-8 2108  ax-9 2116  ax-10 2137  ax-11 2154  ax-12 2171  ax-ext 2703
This theorem depends on definitions:  df-bi 206  df-an 397  df-or 846  df-tru 1544  df-ex 1782  df-nf 1786  df-cleq 2724  df-clel 2810  df-nfc 2885
This theorem is referenced by:  elabgtOLD  3662  elabgOLD  3666  0nelopabOLD  5567  eliunxp  5835  opeliunxp2  5836  tz6.12f  6914  riotaxfrd  7396  opeliunxp2f  8191  cbvixp  8904  boxcutc  8931  ixpiunwdom  9581  rankidb  9791  rankuni2b  9844  acni2  10037  ac6c4  10472  iundom2g  10531  tskuni  10774  reuccatpfxs1  14693  gsumcom2  19837  gsummatr01lem4  22151  ptclsg  23110  cnextfvval  23560  prdsdsf  23864  nnindf  32012  gsumpart  32194  nsgqusf1olem1  32512  nsgqusf1olem3  32514  bnj1463  34054  fineqvrep  34083  ptrest  36475  sdclem1  36599  eqrelf  37111  binomcxplemnotnn0  43100  eliin2f  43778  stoweidlem26  44728  stoweidlem36  44738  stoweidlem46  44748  stoweidlem51  44753  finfdm  45548  eliunxp2  46962  setrec1  47689
  Copyright terms: Public domain W3C validator