Theorem nfel2 2922

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

Step	Hyp	Ref	Expression
1		nfcv 2904	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2918	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1786   ∈ wcel 2107  Ⅎwnfc 2884

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2704

This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-tru 1545  df-ex 1783  df-nf 1787  df-cleq 2725  df-clel 2811  df-nfc 2886

This theorem is referenced by:  elabgtOLD  3664  elabgOLD  3668  0nelopabOLD  5569  eliunxp  5838  opeliunxp2  5839  tz6.12f  6918  riotaxfrd  7400  opeliunxp2f  8195  cbvixp  8908  boxcutc  8935  ixpiunwdom  9585  rankidb  9795  rankuni2b  9848  acni2  10041  ac6c4  10476  iundom2g  10535  tskuni  10778  reuccatpfxs1  14697  gsumcom2  19843  gsummatr01lem4  22160  ptclsg  23119  cnextfvval  23569  prdsdsf  23873  nnindf  32025  gsumpart  32207  nsgqusf1olem1  32524  nsgqusf1olem3  32526  bnj1463  34066  fineqvrep  34095  ptrest  36487  sdclem1  36611  eqrelf  37123  binomcxplemnotnn0  43115  eliin2f  43793  stoweidlem26  44742  stoweidlem36  44752  stoweidlem46  44762  stoweidlem51  44767  finfdm  45562  eliunxp2  47009  setrec1  47736