Theorem nfel2 2927

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

Syntax hints:  Ⅎwnf 1781   ∈ wcel 2108  Ⅎwnfc 2893

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1793  ax-4 1807  ax-5 1909  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2158  ax-12 2178  ax-ext 2711

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 847  df-tru 1540  df-ex 1778  df-nf 1782  df-cleq 2732  df-clel 2819  df-nfc 2895

This theorem is referenced by:  elabgtOLDOLD  3687  elabgOLD  3691  0nelopabOLD  5587  eliunxp  5862  opeliunxp2  5863  tz6.12f  6946  riotaxfrd  7439  opeliunxp2f  8251  cbvixp  8972  boxcutc  8999  ixpiunwdom  9659  rankidb  9869  rankuni2b  9922  acni2  10115  ac6c4  10550  iundom2g  10609  tskuni  10852  reuccatpfxs1  14795  gsumcom2  20017  gsummatr01lem4  22685  ptclsg  23644  cnextfvval  24094  prdsdsf  24398  nnindf  32823  gsumpart  33038  nsgqusf1olem1  33406  nsgqusf1olem3  33408  bnj1463  35031  fineqvrep  35071  ptrest  37579  sdclem1  37703  eqrelf  38211  binomcxplemnotnn0  44325  eliin2f  45006  stoweidlem26  45947  stoweidlem36  45957  stoweidlem46  45967  stoweidlem51  45972  finfdm  46767  eliunxp2  48058  setrec1  48783