Theorem nfel2 2910

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 2891	. 2 ⊢ Ⅎ𝑥𝐴
2		nfeq2.1	. 2 ⊢ Ⅎ𝑥𝐵
3	1, 2	nfel 2906	1 ⊢ Ⅎ𝑥 𝐴 ∈ 𝐵

Syntax hints:  Ⅎwnf 1783   ∈ wcel 2109  Ⅎwnfc 2876

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2008  ax-8 2111  ax-9 2119  ax-10 2142  ax-11 2158  ax-12 2178  ax-ext 2701

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1543  df-ex 1780  df-nf 1784  df-cleq 2721  df-clel 2803  df-nfc 2878

This theorem is referenced by:  eliunxp  5791  opeliunxp2  5792  tz6.12f  6866  riotaxfrd  7360  opeliunxp2f  8166  cbvixp  8864  boxcutc  8891  ixpiunwdom  9519  rankidb  9729  rankuni2b  9782  acni2  9975  ac6c4  10410  iundom2g  10469  tskuni  10712  reuccatpfxs1  14688  gsumcom2  19881  gsummatr01lem4  22521  ptclsg  23478  cnextfvval  23928  prdsdsf  24231  nnindf  32717  gsumpart  32970  nsgqusf1olem1  33357  nsgqusf1olem3  33359  bnj1463  35018  fineqvrep  35058  ptrest  37586  sdclem1  37710  eqrelf  38217  binomcxplemnotnn0  44318  eliin2f  45071  stoweidlem26  45997  stoweidlem36  46007  stoweidlem46  46017  stoweidlem51  46022  sge0f1o  46353  finfdm  46817  eliunxp2  48295  setrec1  49653