Theorem nfel2 2914

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

Syntax hints:  Ⅎwnf 1784   ∈ wcel 2113  Ⅎwnfc 2880

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 1968  ax-7 2009  ax-8 2115  ax-9 2123  ax-10 2146  ax-11 2162  ax-12 2182  ax-ext 2705

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-tru 1544  df-ex 1781  df-nf 1785  df-cleq 2725  df-clel 2808  df-nfc 2882

This theorem is referenced by:  eliunxp  5783  opeliunxp2  5784  tz6.12f  6856  riotaxfrd  7346  opeliunxp2f  8149  cbvixp  8848  boxcutc  8875  ixpiunwdom  9487  rankidb  9704  rankuni2b  9757  acni2  9948  ac6c4  10383  iundom2g  10442  tskuni  10685  reuccatpfxs1  14661  gsumcom2  19895  gsummatr01lem4  22593  ptclsg  23550  cnextfvval  24000  prdsdsf  24302  nnindf  32828  gsumpart  33074  nsgqusf1olem1  33422  nsgqusf1olem3  33424  bnj1463  35139  fineqvrep  35209  ptrest  37732  sdclem1  37856  eqrelf  38365  binomcxplemnotnn0  44513  eliin2f  45264  stoweidlem26  46186  stoweidlem36  46196  stoweidlem46  46206  stoweidlem51  46211  sge0f1o  46542  finfdm  47006  eliunxp2  48496  setrec1  49852