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

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

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