Theorem nfel2 2917

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

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

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 2184  ax-ext 2708

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 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  eliunxp  5786  opeliunxp2  5787  tz6.12f  6859  riotaxfrd  7349  opeliunxp2f  8152  cbvixp  8852  boxcutc  8879  ixpiunwdom  9495  rankidb  9712  rankuni2b  9765  acni2  9956  ac6c4  10391  iundom2g  10450  tskuni  10694  reuccatpfxs1  14670  gsumcom2  19904  gsummatr01lem4  22602  ptclsg  23559  cnextfvval  24009  prdsdsf  24311  nnindf  32900  gsumpart  33146  nsgqusf1olem1  33494  nsgqusf1olem3  33496  bnj1463  35211  fineqvrep  35270  ptrest  37820  sdclem1  37944  eqrelf  38453  binomcxplemnotnn0  44597  eliin2f  45348  stoweidlem26  46270  stoweidlem36  46280  stoweidlem46  46290  stoweidlem51  46295  sge0f1o  46626  finfdm  47090  eliunxp2  48580  setrec1  49936