Theorem nfel2 2918

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

Syntax hints:  Ⅎwnf 1785   ∈ wcel 2114  Ⅎwnfc 2884

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 2709

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 2729  df-clel 2812  df-nfc 2886

This theorem is referenced by:  eliunxp  5794  opeliunxp2  5795  tz6.12f  6867  riotaxfrd  7359  opeliunxp2f  8162  cbvixp  8864  boxcutc  8891  ixpiunwdom  9507  rankidb  9724  rankuni2b  9777  acni2  9968  ac6c4  10403  iundom2g  10462  tskuni  10706  reuccatpfxs1  14682  gsumcom2  19916  gsummatr01lem4  22614  ptclsg  23571  cnextfvval  24021  prdsdsf  24323  nnindf  32911  gsumpart  33157  nsgqusf1olem1  33506  nsgqusf1olem3  33508  bnj1463  35231  fineqvrep  35292  ptrest  37870  sdclem1  37994  eqrelf  38509  binomcxplemnotnn0  44712  eliin2f  45463  stoweidlem26  46384  stoweidlem36  46394  stoweidlem46  46404  stoweidlem51  46409  sge0f1o  46740  finfdm  47204  eliunxp2  48694  setrec1  50050