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 1785   ∈ wcel 2114  Ⅎ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 1912  ax-6 1969  ax-7 2010  ax-8 2116  ax-9 2124  ax-10 2147  ax-11 2163  ax-12 2185  ax-ext 2708

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 849  df-tru 1545  df-ex 1782  df-nf 1786  df-cleq 2728  df-clel 2811  df-nfc 2885

This theorem is referenced by:  eliunxp  5792  opeliunxp2  5793  tz6.12f  6865  riotaxfrd  7358  opeliunxp2f  8160  cbvixp  8862  boxcutc  8889  ixpiunwdom  9505  rankidb  9724  rankuni2b  9777  acni2  9968  ac6c4  10403  iundom2g  10462  tskuni  10706  reuccatpfxs1  14709  gsumcom2  19950  gsummatr01lem4  22623  ptclsg  23580  cnextfvval  24030  prdsdsf  24332  nnindf  32893  gsumpart  33124  nsgqusf1olem1  33473  nsgqusf1olem3  33475  bnj1463  35197  fineqvrep  35258  ptrest  37940  sdclem1  38064  eqrelf  38579  binomcxplemnotnn0  44783  eliin2f  45534  stoweidlem26  46454  stoweidlem36  46464  stoweidlem46  46474  stoweidlem51  46479  sge0f1o  46810  finfdm  47274  eliunxp2  48810  setrec1  50166