Theorem nfel2 2941

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

Syntax hints:  Ⅎwnf 1802   ∈ wcel 2141  Ⅎwnfc 2908

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1814  ax-4 1828  ax-5 1929  ax-6 1986  ax-7 2027  ax-8 2143  ax-9 2151  ax-10 2174  ax-11 2190  ax-12 2211  ax-ext 2733

This theorem depends on definitions:  df-bi 209  df-an 400  df-or 859  df-tru 1562  df-ex 1799  df-nf 1803  df-cleq 2753  df-clel 2836  df-nfc 2910

This theorem is referenced by:  eliunxp  5805  opeliunxp2  5806  tz6.12f  6887  riotaxfrd  7382  opeliunxp2f  8184  cbvixp  8890  boxcutc  8917  ixpiunwdom  9532  rankidb  9752  rankuni2b  9805  acni2  9996  ac6c4  10432  iundom2g  10491  tskuni  10735  reuccatpfxs1  14754  gsumcom2  20006  gsummatr01lem4  22706  ptclsg  23663  cnextfvval  24113  prdsdsf  24415  nnindf  32983  gsumpart  33204  nsgqusf1olem1  33560  nsgqusf1olem3  33562  bnj1463  35311  fineqvrep  35371  ptrest  38079  sdclem1  38203  eqrelf  38718  binomcxplemnotnn0  44893  eliin2f  45643  stoweidlem26  46561  stoweidlem36  46571  stoweidlem46  46581  stoweidlem51  46586  sge0f1o  46917  finfdm  47381  eliunxp2  48917  setrec1  50273