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

Theorem nfel2 2998
 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 2979 . 2 𝑥𝐴
2 nfeq2.1 . 2 𝑥𝐵
31, 2nfel 2994 1 𝑥 𝐴𝐵
 Colors of variables: wff setvar class Syntax hints:  Ⅎwnf 1784   ∈ wcel 2114  Ⅎwnfc 2963 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1796  ax-4 1810  ax-5 1911  ax-6 1970  ax-7 2015  ax-8 2116  ax-9 2124  ax-10 2145  ax-11 2161  ax-12 2177  ax-ext 2795 This theorem depends on definitions:  df-bi 209  df-an 399  df-or 844  df-tru 1540  df-ex 1781  df-nf 1785  df-cleq 2816  df-clel 2895  df-nfc 2965 This theorem is referenced by:  elabgt  3665  elabg  3668  opelopabsb  5419  0nelopab  5454  eliunxp  5710  opeliunxp2  5711  tz6.12f  6696  riotaxfrd  7150  opeliunxp2f  7878  cbvixp  8480  boxcutc  8507  ixpiunwdom  9057  rankidb  9231  rankuni2b  9284  acni2  9474  ac6c4  9905  iundom2g  9964  tskuni  10207  reuccatpfxs1  14111  gsumcom2  19097  gsummatr01lem4  21269  ptclsg  22225  cnextfvval  22675  prdsdsf  22979  nnindf  30537  bnj1463  32329  ptrest  34893  sdclem1  35020  eqrelf  35519  binomcxplemnotnn0  40695  eliin2f  41377  stoweidlem26  42318  stoweidlem36  42328  stoweidlem46  42338  stoweidlem51  42343  eliunxp2  44389  setrec1  44801
 Copyright terms: Public domain W3C validator