Theorem nfel2 2943

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

Syntax hints:  Ⅎwnf 1813   ∈ wcel 2143  Ⅎwnfc 2910

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1825  ax-4 1839  ax-5 1940  ax-6 1997  ax-7 2038  ax-8 2145  ax-9 2153  ax-10 2176  ax-11 2192  ax-12 2213  ax-ext 2735

This theorem depends on definitions:  df-bi 210  df-an 401  df-or 861  df-tru 1573  df-ex 1810  df-nf 1814  df-cleq 2755  df-clel 2838  df-nfc 2912

This theorem is referenced by:  eliunxp  5823  opeliunxp2  5824  tz6.12f  6906  riotaxfrd  7401  opeliunxp2f  8202  cbvixp  8908  boxcutc  8935  ixpiunwdom  9548  rankidb  9768  rankuni2b  9821  acni2  10026  ac6c4  10460  iundom2g  10519  tskuni  10763  reuccatpfxs1  14780  gsumcom2  20040  gsummatr01lem4  22815  ptclsg  23772  cnextfvval  24222  prdsdsf  24524  nnindf  33164  gsumpart  33383  nsgqusf1olem1  33722  nsgqusf1olem3  33724  bnj1463  35443  fineqvrep  35527  ptrest  38270  sdclem1  38394  eqrelf  38907  binomcxplemnotnn0  45066  eliin2f  45822  stoweidlem26  46740  stoweidlem36  46750  stoweidlem46  46760  stoweidlem51  46765  sge0f1o  47096  finfdm  47560  eliunxp2  49114  setrec1  50469